- apply cast; apply Imply_intro; intro;
- apply cast; apply Forall_intro; intro z;
- apply cast; apply Imply_intro; intro;
- apply cast; apply (Exists_elim N (λy.R y z)); try intros (n);
- [ apply cast; assumption
- | apply cast; apply (Exists_intro ? ? n);
- apply cast; apply (Imply_elim (R n z) (R z n));
- [ apply cast; apply (Forall_elim N (λb:N.R n b ⇒ R b n) z);
- apply cast; apply (Forall_elim N (λa:N.∀b:N.R a b ⇒ R b a) n);
- apply cast; assumption
- | apply cast; assumption
+ apply cast;
+ apply (⇒\sub\i [H] (∀z:N.(∃x:N.R x z)⇒∃y:N.R z y));
+ apply (∀\sub\i [z] ((∃x:N.R x z)⇒∃y:N.R z y));
+ apply (⇒\sub\i [H2] (∃y:N.R z y));
+ apply (∃\sub\e (∃x:N.R x z) [n] [H3] (∃y:N.R z y));
+ [ apply [H2]
+ | apply (∃\sub\i n (R z n));
+ apply (⇒\sub\e (R n z ⇒ R z n) (R n z));
+ [ apply (∀\sub\e (∀b:N.R n b ⇒ R b n));
+ apply (∀\sub\e (∀a:N.∀b:N.R a b ⇒ R b a));
+ apply [H]
+ | apply [H3]