example.agda

--                   ------ u           
--                      P              
--                   ------ ∧I          ------- k
--                    P × P               R
--                   ------------- ∨I2  ------- ∨I₁
--                    (R ⊎ (P × P))    (R ⊎ (P × P)) 
--     k ----------  -------------------------------
--         (P ⊎ R)           (R ⊎ (P × P))
--   ∨Eᵘᵐ ----------------------------------
--           (R ⊎ (P × P))
--    I→ᵏ -------------------------- 
--         (P ⊎ R) → (R ⊎ (P × P))
--
thm : ∀ (P R : Set) → (P ⊎ R) → (R ⊎ (P × P))
thm P R (inj₁ ev_P) =  inj₂ ⟨ ev_P , ev_P ⟩
thm P R (inj₂ ev_R) =  inj₁ ev_R