Section p2p1_. Let false:=False. Let false_ind:=False_ind. Variable dom:Set. Variable col:dom->dom->dom->dom->Prop. Variable el:dom->dom->Prop. Variable ep:dom->dom->Prop. Variable goal:Prop. Variable pl:dom->dom->Prop. Variable a b c d e f g h i l m n o p q r s:dom. Hypothesis assump1:(col a b c l)/\(col d e f m). Hypothesis assump2:(col b f g n)/\(col c e g o). Hypothesis assump3:(col b d h p)/\(col a e h q). Hypothesis assump4:(col c d i r)/\(col a f i s). Hypothesis goalam:(pl a m)->goal. Hypothesis goalbm:(pl b m)->goal. Hypothesis goalcm:(pl c m)->goal. Hypothesis goaldl:(pl d l)->goal. Hypothesis goalel:(pl e l)->goal. Hypothesis goalfl:(pl f l)->goal. Hypothesis goal4:forall A:dom,(pl g A)/\(pl h A)/\(pl i A)->goal. Hypothesis col_elim1:forall A B C D:dom,(col A B C D)->(pl A D). Hypothesis col_elim2:forall A B C D:dom,(col A B C D)->(pl B D). Hypothesis col_elim3:forall A B C D:dom,(col A B C D)->(pl C D). Hypothesis pref:forall A B:dom,(pl A B)->(ep A A). Hypothesis psym:forall A B:dom,(ep A B)->(ep B A). Hypothesis ptra:forall A B C:dom,(ep A B)/\(ep B C)->(ep A C). Hypothesis lref:forall A B:dom,(pl A B)->(el B B). Hypothesis lsym:forall A B:dom,(el A B)->(el B A). Hypothesis ltra:forall A B C:dom,(el A B)/\(el B C)->(el A C). Hypothesis pcon:forall A B C:dom,(ep A B)/\(pl B C)->(pl A C). Hypothesis lcon:forall A B C:dom,(pl A B)/\(el B C)->(pl A C). Hypothesis papp1:forall A B C D E F G H I J K L M N O P Q:dom,(col A B C J)/\(col D E F K)/\(col B F G L)/\(col C E G M)/\(col B D H N)/\(col A E H O)/\(col C D I P)/\(col A F I Q)->(exists R:dom,(col G H I R)) \/ (el L M) \/ (el N O) \/ (el P Q). Hypothesis unique:forall A B C D:dom,(pl C A)/\(pl C B)/\(pl D A)/\(pl D B)->(ep C D) \/ (el A B). Hypothesis line:forall A B:dom,(ep A A)/\(ep B B)->(exists C:dom,(pl A C)/\(pl B C)). Hypothesis point:forall A B C:dom,(el C C)/\(el B B)->(exists A:dom,(pl A B)/\(pl A C)). Lemma p2p1_1: (col a b c l)/\(col d e f m). Proof. exact (assump1). Qed. Lemma p2p1_2: (col b f g n)/\(col c e g o). Proof. exact (assump2). Qed. Lemma p2p1_3: (col b d h p)/\(col a e h q). Proof. exact (assump3). Qed. Lemma p2p1_4: (col c d i r)/\(col a f i s). Proof. exact (assump4). Qed. Lemma p2p1_5: (pl a l). Proof. exact (((col_elim1 a b c l) (proj1 p2p1_1))). Qed. Lemma p2p1_6: (pl d m). Proof. exact (((col_elim1 d e f m) (proj2 p2p1_1))). Qed. Lemma p2p1_7: (pl b n). Proof. exact (((col_elim1 b f g n) (proj1 p2p1_2))). Qed. Lemma p2p1_8: (pl c o). Proof. exact (((col_elim1 c e g o) (proj2 p2p1_2))). Qed. Lemma p2p1_9: (pl b p). Proof. exact (((col_elim1 b d h p) (proj1 p2p1_3))). Qed. Lemma p2p1_10: (pl a q). Proof. exact (((col_elim1 a e h q) (proj2 p2p1_3))). Qed. Lemma p2p1_11: (pl c r). Proof. exact (((col_elim1 c d i r) (proj1 p2p1_4))). Qed. Lemma p2p1_12: (pl a s). Proof. exact (((col_elim1 a f i s) (proj2 p2p1_4))). Qed. Lemma p2p1_13: (pl b l). Proof. exact (((col_elim2 a b c l) (proj1 p2p1_1))). Qed. Lemma p2p1_14: (pl e m). Proof. exact (((col_elim2 d e f m) (proj2 p2p1_1))). Qed. Lemma p2p1_15: (pl f n). Proof. exact (((col_elim2 b f g n) (proj1 p2p1_2))). Qed. Lemma p2p1_16: (pl e o). Proof. exact (((col_elim2 c e g o) (proj2 p2p1_2))). Qed. Lemma p2p1_17: (pl d p). Proof. exact (((col_elim2 b d h p) (proj1 p2p1_3))). Qed. Lemma p2p1_18: (pl e q). Proof. exact (((col_elim2 a e h q) (proj2 p2p1_3))). Qed. Lemma p2p1_19: (pl d r). Proof. exact (((col_elim2 c d i r) (proj1 p2p1_4))). Qed. Lemma p2p1_20: (pl f s). Proof. exact (((col_elim2 a f i s) (proj2 p2p1_4))). Qed. Lemma p2p1_21: (pl c l). Proof. exact (((col_elim3 a b c l) (proj1 p2p1_1))). Qed. Lemma p2p1_22: (pl f m). Proof. exact (((col_elim3 d e f m) (proj2 p2p1_1))). Qed. Lemma p2p1_23: (pl g n). Proof. exact (((col_elim3 b f g n) (proj1 p2p1_2))). Qed. Lemma p2p1_24: (pl g o). Proof. exact (((col_elim3 c e g o) (proj2 p2p1_2))). Qed. Lemma p2p1_25: (pl h p). Proof. exact (((col_elim3 b d h p) (proj1 p2p1_3))). Qed. Lemma p2p1_26: (pl h q). Proof. exact (((col_elim3 a e h q) (proj2 p2p1_3))). Qed. Lemma p2p1_27: (pl i r). Proof. exact (((col_elim3 c d i r) (proj1 p2p1_4))). Qed. Lemma p2p1_28: (pl i s). Proof. exact (((col_elim3 a f i s) (proj2 p2p1_4))). Qed. Lemma p2p1_29: (ep a a). Proof. exact (((pref a l) p2p1_5)). Qed. Lemma p2p1_30: (ep d d). Proof. exact (((pref d m) p2p1_6)). Qed. Lemma p2p1_31: (ep b b). Proof. exact (((pref b n) p2p1_7)). Qed. Lemma p2p1_32: (ep c c). Proof. exact (((pref c o) p2p1_8)). Qed. Lemma p2p1_33: (ep e e). Proof. exact (((pref e m) p2p1_14)). Qed. Lemma p2p1_34: (ep f f). Proof. exact (((pref f n) p2p1_15)). Qed. Lemma p2p1_35: (ep g g). Proof. exact (((pref g n) p2p1_23)). Qed. Lemma p2p1_36: (ep h h). Proof. exact (((pref h p) p2p1_25)). Qed. Lemma p2p1_37: (ep i i). Proof. exact (((pref i r) p2p1_27)). Qed. Lemma p2p1_46: (exists A:dom,(col g h i A)) \/ (el n o) \/ (el p q) \/ (el r s). Proof. exact (((papp1 a b c d e f g h i l m n o p q r s) (conj (proj1 p2p1_1) (conj (proj2 p2p1_1) (conj (proj1 p2p1_2) (conj (proj2 p2p1_2) (conj (proj1 p2p1_3) (conj (proj2 p2p1_3) (conj (proj1 p2p1_4) (proj2 p2p1_4)))))))))). Qed. Lemma p2p1_47: forall C0:dom,(col g h i C0)->(pl g C0). Proof. exact (fun (C0:dom)(VcolghiC0:(col g h i C0))=>((col_elim1 g h i C0) VcolghiC0)). Qed. Lemma p2p1_48: forall C0:dom,(col g h i C0)->(pl h C0). Proof. exact (fun (C0:dom)(VcolghiC0:(col g h i C0))=>((col_elim2 g h i C0) VcolghiC0)). Qed. Lemma p2p1_49: forall C0:dom,(col g h i C0)->(pl i C0). Proof. exact (fun (C0:dom)(VcolghiC0:(col g h i C0))=>((col_elim3 g h i C0) VcolghiC0)). Qed. Lemma p2p1_50: forall C0:dom,(col g h i C0)->goal. Proof. exact (fun (C0:dom)(VcolghiC0:(col g h i C0))=>((goal4 C0) (conj (p2p1_47 C0 VcolghiC0) (conj (p2p1_48 C0 VcolghiC0) (p2p1_49 C0 VcolghiC0))))). Qed. Lemma p2p1_51: (el n o)->(el o n). Proof. exact (fun (Velno:(el n o))=>((lsym n o) Velno)). Qed. Lemma p2p1_53: (el n o)->(pl c n). Proof. exact (fun (Velno:(el n o))=>((lcon c o n) (conj p2p1_8 (p2p1_51 Velno)))). Qed. Lemma p2p1_54: (el n o)->(pl f o). Proof. exact (fun (Velno:(el n o))=>((lcon f n o) (conj p2p1_15 Velno))). Qed. Lemma p2p1_56: (el n o)->(ep b c) \/ (el n l). Proof. exact (fun (Velno:(el n o))=>((unique n l b c) (conj p2p1_7 (conj p2p1_13 (conj (p2p1_53 Velno) p2p1_21))))). Qed. Lemma p2p1_58: (el n o)->(ep b c)->(pl b r). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))=>((pcon b c r) (conj Vepbc p2p1_11))). Qed. Lemma p2p1_60: (el n o)->(ep b c)->(ep b d) \/ (el p r). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))=>((unique p r b d) (conj p2p1_9 (conj (p2p1_58 Velno Vepbc) (conj p2p1_17 p2p1_19))))). Qed. Lemma p2p1_64: (el n o)->(ep b c)->(ep b d)->(pl b m). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Vepbd:(ep b d))=>((pcon b d m) (conj Vepbd p2p1_6))). Qed. Lemma p2p1_65: (el n o)->(ep b c)->(ep b d)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Vepbd:(ep b d))=>(goalbm (p2p1_64 Velno Vepbc Vepbd))). Qed. Lemma p2p1_66: (el n o)->(ep b c)->(el p r)->(el r p). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))=>((lsym p r) Velpr)). Qed. Lemma p2p1_68: (el n o)->(ep b c)->(el p r)->(pl i p). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))=>((lcon i r p) (conj p2p1_27 (p2p1_66 Velno Vepbc Velpr)))). Qed. Lemma p2p1_69: (el n o)->(ep b c)->(el p r)->(ep e f) \/ (el m o). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))=>((unique m o e f) (conj p2p1_14 (conj p2p1_16 (conj p2p1_22 (p2p1_54 Velno)))))). Qed. Lemma p2p1_70: (el n o)->(ep b c)->(el p r)->(ep e f)->(ep f e). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))=>((psym e f) Vepef)). Qed. Lemma p2p1_71: (el n o)->(ep b c)->(el p r)->(ep e f)->(pl e s). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))=>((pcon e f s) (conj Vepef p2p1_20))). Qed. Lemma p2p1_73: (el n o)->(ep b c)->(el p r)->(ep e f)->(ep a e) \/ (el q s). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))=>((unique q s a e) (conj p2p1_10 (conj p2p1_12 (conj p2p1_18 (p2p1_71 Velno Vepbc Velpr Vepef)))))). Qed. Lemma p2p1_77: (el n o)->(ep b c)->(el p r)->(ep e f)->(ep a e)->(pl a m). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Vepae:(ep a e))=>((pcon a e m) (conj Vepae p2p1_14))). Qed. Lemma p2p1_78: (el n o)->(ep b c)->(el p r)->(ep e f)->(ep a e)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Vepae:(ep a e))=>(goalam (p2p1_77 Velno Vepbc Velpr Vepef Vepae))). Qed. Lemma p2p1_79: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el s q). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))=>((lsym q s) Velqs)). Qed. Lemma p2p1_81: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(pl i q). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))=>((lcon i s q) (conj p2p1_28 (p2p1_79 Velno Vepbc Velpr Vepef Velqs)))). Qed. Lemma p2p1_82: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(ep h i) \/ (el p q). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))=>((unique p q h i) (conj p2p1_25 (conj p2p1_26 (conj (p2p1_68 Velno Vepbc Velpr) (p2p1_81 Velno Vepbc Velpr Vepef Velqs)))))). Qed. Lemma p2p1_83: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(ep h i)->(ep i h). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Vephi:(ep h i))=>((psym h i) Vephi)). Qed. Lemma p2p1_84: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(ep h i)->(exists A:dom,(pl a A)/\(pl d A)). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Vephi:(ep h i))=>((line a d) (conj p2p1_29 p2p1_30))). Qed. Lemma p2p1_86: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(ep h i)->forall C0:dom,(pl a C0)->(pl d C0)->(exists A:dom,(pl a A)/\(pl g A)). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Vephi:(ep h i))(C0:dom)(VplaC0:(pl a C0))(VpldC0:(pl d C0))=>((line a g) (conj p2p1_29 p2p1_35))). Qed. Lemma p2p1_88: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(ep h i)->forall C0:dom,(pl a C0)->(pl d C0)->forall C1:dom,(pl a C1)->(pl g C1)->(exists A:dom,(pl d A)/\(pl g A)). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Vephi:(ep h i))(C0:dom)(VplaC0:(pl a C0))(VpldC0:(pl d C0))(C1:dom)(VplaC1:(pl a C1))(VplgC1:(pl g C1))=>((line d g) (conj p2p1_30 p2p1_35))). Qed. Lemma p2p1_90: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(ep h i)->forall C0:dom,(pl a C0)->(pl d C0)->forall C1:dom,(pl a C1)->(pl g C1)->forall C2:dom,(pl d C2)->(pl g C2)->(exists A:dom,(pl g A)/\(pl h A)). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Vephi:(ep h i))(C0:dom)(VplaC0:(pl a C0))(VpldC0:(pl d C0))(C1:dom)(VplaC1:(pl a C1))(VplgC1:(pl g C1))(C2:dom)(VpldC2:(pl d C2))(VplgC2:(pl g C2))=>((line g h) (conj p2p1_35 p2p1_36))). Qed. Lemma p2p1_92: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(ep h i)->forall C0:dom,(pl a C0)->(pl d C0)->forall C1:dom,(pl a C1)->(pl g C1)->forall C2:dom,(pl d C2)->(pl g C2)->forall C3:dom,(pl g C3)->(pl h C3)->(pl i C3). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Vephi:(ep h i))(C0:dom)(VplaC0:(pl a C0))(VpldC0:(pl d C0))(C1:dom)(VplaC1:(pl a C1))(VplgC1:(pl g C1))(C2:dom)(VpldC2:(pl d C2))(VplgC2:(pl g C2))(C3:dom)(VplgC3:(pl g C3))(VplhC3:(pl h C3))=>((pcon i h C3) (conj (p2p1_83 Velno Vepbc Velpr Vepef Velqs Vephi) VplhC3))). Qed. Lemma p2p1_93: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(ep h i)->forall C0:dom,(pl a C0)->(pl d C0)->forall C1:dom,(pl a C1)->(pl g C1)->forall C2:dom,(pl d C2)->(pl g C2)->forall C3:dom,(pl g C3)->(pl h C3)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Vephi:(ep h i))(C0:dom)(VplaC0:(pl a C0))(VpldC0:(pl d C0))(C1:dom)(VplaC1:(pl a C1))(VplgC1:(pl g C1))(C2:dom)(VpldC2:(pl d C2))(VplgC2:(pl g C2))(C3:dom)(VplgC3:(pl g C3))(VplhC3:(pl h C3))=>((goal4 C3) (conj VplgC3 (conj VplhC3 (p2p1_92 Velno Vepbc Velpr Vepef Velqs Vephi C0 VplaC0 VpldC0 C1 VplaC1 VplgC1 C2 VpldC2 VplgC2 C3 VplgC3 VplhC3))))). Qed. Lemma p2p1_94: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(ep h i)->forall C0:dom,(pl a C0)->(pl d C0)->forall C1:dom,(pl a C1)->(pl g C1)->forall C2:dom,(pl d C2)->(pl g C2)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Vephi:(ep h i))(C0:dom)(VplaC0:(pl a C0))(VpldC0:(pl d C0))(C1:dom)(VplaC1:(pl a C1))(VplgC1:(pl g C1))(C2:dom)(VpldC2:(pl d C2))(VplgC2:(pl g C2))=>((ex_ind (P:=fun C3:dom=>(pl g C3)/\(pl h C3))(fun C3:dom=>(and_ind (p2p1_93 Velno Vepbc Velpr Vepef Velqs Vephi C0 VplaC0 VpldC0 C1 VplaC1 VplgC1 C2 VpldC2 VplgC2 C3))))(p2p1_90 Velno Vepbc Velpr Vepef Velqs Vephi C0 VplaC0 VpldC0 C1 VplaC1 VplgC1 C2 VpldC2 VplgC2))). Qed. Lemma p2p1_95: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(ep h i)->forall C0:dom,(pl a C0)->(pl d C0)->forall C1:dom,(pl a C1)->(pl g C1)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Vephi:(ep h i))(C0:dom)(VplaC0:(pl a C0))(VpldC0:(pl d C0))(C1:dom)(VplaC1:(pl a C1))(VplgC1:(pl g C1))=>((ex_ind (P:=fun C2:dom=>(pl d C2)/\(pl g C2))(fun C2:dom=>(and_ind (p2p1_94 Velno Vepbc Velpr Vepef Velqs Vephi C0 VplaC0 VpldC0 C1 VplaC1 VplgC1 C2))))(p2p1_88 Velno Vepbc Velpr Vepef Velqs Vephi C0 VplaC0 VpldC0 C1 VplaC1 VplgC1))). Qed. Lemma p2p1_96: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(ep h i)->forall C0:dom,(pl a C0)->(pl d C0)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Vephi:(ep h i))(C0:dom)(VplaC0:(pl a C0))(VpldC0:(pl d C0))=>((ex_ind (P:=fun C1:dom=>(pl a C1)/\(pl g C1))(fun C1:dom=>(and_ind (p2p1_95 Velno Vepbc Velpr Vepef Velqs Vephi C0 VplaC0 VpldC0 C1))))(p2p1_86 Velno Vepbc Velpr Vepef Velqs Vephi C0 VplaC0 VpldC0))). Qed. Lemma p2p1_97: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(ep h i)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Vephi:(ep h i))=>((ex_ind (P:=fun C0:dom=>(pl a C0)/\(pl d C0))(fun C0:dom=>(and_ind (p2p1_96 Velno Vepbc Velpr Vepef Velqs Vephi C0))))(p2p1_84 Velno Vepbc Velpr Vepef Velqs Vephi))). Qed. Lemma p2p1_98: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(el q p). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))=>((lsym p q) Velpq)). Qed. Lemma p2p1_105: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(pl b q). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))=>((lcon b p q) (conj p2p1_9 Velpq))). Qed. Lemma p2p1_113: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(pl e p). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))=>((lcon e q p) (conj p2p1_18 (p2p1_98 Velno Vepbc Velpr Vepef Velqs Velpq)))). Qed. Lemma p2p1_114: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(pl f p). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))=>((pcon f e p) (conj (p2p1_70 Velno Vepbc Velpr Vepef) (p2p1_113 Velno Vepbc Velpr Vepef Velqs Velpq)))). Qed. Lemma p2p1_117: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(ep a b) \/ (el l q). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))=>((unique l q a b) (conj p2p1_5 (conj p2p1_10 (conj p2p1_13 (p2p1_105 Velno Vepbc Velpr Vepef Velqs Velpq)))))). Qed. Lemma p2p1_123: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(ep a b)->(ep d e) \/ (el m p). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vepab:(ep a b))=>((unique m p d e) (conj p2p1_6 (conj p2p1_17 (conj p2p1_14 (p2p1_113 Velno Vepbc Velpr Vepef Velqs Velpq)))))). Qed. Lemma p2p1_129: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(ep a b)->(ep d e)->(ep b f) \/ (el n p). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))=>((unique n p b f) (conj p2p1_7 (conj p2p1_9 (conj p2p1_15 (p2p1_114 Velno Vepbc Velpr Vepef Velqs Velpq)))))). Qed. Lemma p2p1_147: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(ep a b)->(ep d e)->(ep b f)->(pl b m). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Vepbf:(ep b f))=>((pcon b f m) (conj Vepbf p2p1_22))). Qed. Lemma p2p1_148: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(ep a b)->(ep d e)->(ep b f)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Vepbf:(ep b f))=>(goalbm (p2p1_147 Velno Vepbc Velpr Vepef Velqs Velpq Vepab Vepde Vepbf))). Qed. Lemma p2p1_164: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(ep a b)->(ep d e)->(el n p)->(pl g p). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velnp:(el n p))=>((lcon g n p) (conj p2p1_23 Velnp))). Qed. Lemma p2p1_165: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(ep a b)->(ep d e)->(el n p)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velnp:(el n p))=>((goal4 p) (conj (p2p1_164 Velno Vepbc Velpr Vepef Velqs Velpq Vepab Vepde Velnp) (conj p2p1_25 (p2p1_68 Velno Vepbc Velpr))))). Qed. Lemma p2p1_166: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(ep a b)->(ep d e)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))=>((or_ind ((p2p1_148 Velno Vepbc Velpr Vepef Velqs Velpq Vepab Vepde))((p2p1_165 Velno Vepbc Velpr Vepef Velqs Velpq Vepab Vepde)))(p2p1_129 Velno Vepbc Velpr Vepef Velqs Velpq Vepab Vepde))). Qed. Lemma p2p1_167: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(ep a b)->(el m p)->(el p m). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vepab:(ep a b))(Velmp:(el m p))=>((lsym m p) Velmp)). Qed. Lemma p2p1_174: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(ep a b)->(el m p)->(pl b m). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vepab:(ep a b))(Velmp:(el m p))=>((lcon b p m) (conj p2p1_9 (p2p1_167 Velno Vepbc Velpr Vepef Velqs Velpq Vepab Velmp)))). Qed. Lemma p2p1_175: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(ep a b)->(el m p)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vepab:(ep a b))(Velmp:(el m p))=>(goalbm (p2p1_174 Velno Vepbc Velpr Vepef Velqs Velpq Vepab Velmp))). Qed. Lemma p2p1_176: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(ep a b)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vepab:(ep a b))=>((or_ind ((p2p1_166 Velno Vepbc Velpr Vepef Velqs Velpq Vepab))((p2p1_175 Velno Vepbc Velpr Vepef Velqs Velpq Vepab)))(p2p1_123 Velno Vepbc Velpr Vepef Velqs Velpq Vepab))). Qed. Lemma p2p1_177: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(el l q)->(el q l). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vellq:(el l q))=>((lsym l q) Vellq)). Qed. Lemma p2p1_180: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(el l q)->(el p l). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vellq:(el l q))=>((ltra p q l) (conj Velpq (p2p1_177 Velno Vepbc Velpr Vepef Velqs Velpq Vellq)))). Qed. Lemma p2p1_184: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(el l q)->(pl d l). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vellq:(el l q))=>((lcon d p l) (conj p2p1_17 (p2p1_180 Velno Vepbc Velpr Vepef Velqs Velpq Vellq)))). Qed. Lemma p2p1_185: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->(el l q)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))(Vellq:(el l q))=>(goaldl (p2p1_184 Velno Vepbc Velpr Vepef Velqs Velpq Vellq))). Qed. Lemma p2p1_186: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->(el p q)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))(Velpq:(el p q))=>((or_ind ((p2p1_176 Velno Vepbc Velpr Vepef Velqs Velpq))((p2p1_185 Velno Vepbc Velpr Vepef Velqs Velpq)))(p2p1_117 Velno Vepbc Velpr Vepef Velqs Velpq))). Qed. Lemma p2p1_187: (el n o)->(ep b c)->(el p r)->(ep e f)->(el q s)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))(Velqs:(el q s))=>((or_ind ((p2p1_97 Velno Vepbc Velpr Vepef Velqs))((p2p1_186 Velno Vepbc Velpr Vepef Velqs)))(p2p1_82 Velno Vepbc Velpr Vepef Velqs))). Qed. Lemma p2p1_188: (el n o)->(ep b c)->(el p r)->(ep e f)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Vepef:(ep e f))=>((or_ind ((p2p1_78 Velno Vepbc Velpr Vepef))((p2p1_187 Velno Vepbc Velpr Vepef)))(p2p1_73 Velno Vepbc Velpr Vepef))). Qed. Lemma p2p1_189: (el n o)->(ep b c)->(el p r)->(el m o)->(el o m). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Velmo:(el m o))=>((lsym m o) Velmo)). Qed. Lemma p2p1_190: (el n o)->(ep b c)->(el p r)->(el m o)->(el n m). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Velmo:(el m o))=>((ltra n o m) (conj Velno (p2p1_189 Velno Vepbc Velpr Velmo)))). Qed. Lemma p2p1_194: (el n o)->(ep b c)->(el p r)->(el m o)->(pl b m). Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Velmo:(el m o))=>((lcon b n m) (conj p2p1_7 (p2p1_190 Velno Vepbc Velpr Velmo)))). Qed. Lemma p2p1_195: (el n o)->(ep b c)->(el p r)->(el m o)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))(Velmo:(el m o))=>(goalbm (p2p1_194 Velno Vepbc Velpr Velmo))). Qed. Lemma p2p1_196: (el n o)->(ep b c)->(el p r)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))(Velpr:(el p r))=>((or_ind ((p2p1_188 Velno Vepbc Velpr))((p2p1_195 Velno Vepbc Velpr)))(p2p1_69 Velno Vepbc Velpr))). Qed. Lemma p2p1_197: (el n o)->(ep b c)->goal. Proof. exact (fun (Velno:(el n o))(Vepbc:(ep b c))=>((or_ind ((p2p1_65 Velno Vepbc))((p2p1_196 Velno Vepbc)))(p2p1_60 Velno Vepbc))). Qed. Lemma p2p1_203: (el n o)->(el n l)->(pl f l). Proof. exact (fun (Velno:(el n o))(Velnl:(el n l))=>((lcon f n l) (conj p2p1_15 Velnl))). Qed. Lemma p2p1_204: (el n o)->(el n l)->goal. Proof. exact (fun (Velno:(el n o))(Velnl:(el n l))=>(goalfl (p2p1_203 Velno Velnl))). Qed. Lemma p2p1_205: (el n o)->goal. Proof. exact (fun (Velno:(el n o))=>((or_ind ((p2p1_197 Velno))((p2p1_204 Velno)))(p2p1_56 Velno))). Qed. Lemma p2p1_206: (el p q)->(el q p). Proof. exact (fun (Velpq:(el p q))=>((lsym p q) Velpq)). Qed. Lemma p2p1_207: (el p q)->(pl b q). Proof. exact (fun (Velpq:(el p q))=>((lcon b p q) (conj p2p1_9 Velpq))). Qed. Lemma p2p1_210: (el p q)->(pl e p). Proof. exact (fun (Velpq:(el p q))=>((lcon e q p) (conj p2p1_18 (p2p1_206 Velpq)))). Qed. Lemma p2p1_211: (el p q)->(ep a b) \/ (el l q). Proof. exact (fun (Velpq:(el p q))=>((unique l q a b) (conj p2p1_5 (conj p2p1_10 (conj p2p1_13 (p2p1_207 Velpq)))))). Qed. Lemma p2p1_212: (el p q)->(ep a b)->(ep b a). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))=>((psym a b) Vepab)). Qed. Lemma p2p1_214: (el p q)->(ep a b)->(pl b s). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))=>((pcon b a s) (conj (p2p1_212 Velpq Vepab) p2p1_12))). Qed. Lemma p2p1_215: (el p q)->(ep a b)->(ep d e) \/ (el m p). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))=>((unique m p d e) (conj p2p1_6 (conj p2p1_17 (conj p2p1_14 (p2p1_210 Velpq)))))). Qed. Lemma p2p1_216: (el p q)->(ep a b)->(ep d e)->(ep e d). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))=>((psym d e) Vepde)). Qed. Lemma p2p1_218: (el p q)->(ep a b)->(ep d e)->(pl e r). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))=>((pcon e d r) (conj (p2p1_216 Velpq Vepab Vepde) p2p1_19))). Qed. Lemma p2p1_219: (el p q)->(ep a b)->(ep d e)->(ep b f) \/ (el n s). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))=>((unique n s b f) (conj p2p1_7 (conj (p2p1_214 Velpq Vepab) (conj p2p1_15 p2p1_20))))). Qed. Lemma p2p1_223: (el p q)->(ep a b)->(ep d e)->(ep b f)->(pl b m). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Vepbf:(ep b f))=>((pcon b f m) (conj Vepbf p2p1_22))). Qed. Lemma p2p1_224: (el p q)->(ep a b)->(ep d e)->(ep b f)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Vepbf:(ep b f))=>(goalbm (p2p1_223 Velpq Vepab Vepde Vepbf))). Qed. Lemma p2p1_225: (el p q)->(ep a b)->(ep d e)->(el n s)->(el s n). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))=>((lsym n s) Velns)). Qed. Lemma p2p1_227: (el p q)->(ep a b)->(ep d e)->(el n s)->(pl i n). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))=>((lcon i s n) (conj p2p1_28 (p2p1_225 Velpq Vepab Vepde Velns)))). Qed. Lemma p2p1_228: (el p q)->(ep a b)->(ep d e)->(el n s)->(ep c e) \/ (el o r). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))=>((unique o r c e) (conj p2p1_8 (conj p2p1_11 (conj p2p1_16 (p2p1_218 Velpq Vepab Vepde)))))). Qed. Lemma p2p1_232: (el p q)->(ep a b)->(ep d e)->(el n s)->(ep c e)->(pl c m). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Vepce:(ep c e))=>((pcon c e m) (conj Vepce p2p1_14))). Qed. Lemma p2p1_233: (el p q)->(ep a b)->(ep d e)->(el n s)->(ep c e)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Vepce:(ep c e))=>(goalcm (p2p1_232 Velpq Vepab Vepde Velns Vepce))). Qed. Lemma p2p1_234: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el r o). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))=>((lsym o r) Velor)). Qed. Lemma p2p1_236: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(pl i o). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))=>((lcon i r o) (conj p2p1_27 (p2p1_234 Velpq Vepab Vepde Velns Velor)))). Qed. Lemma p2p1_237: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(ep g i) \/ (el n o). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))=>((unique n o g i) (conj p2p1_23 (conj p2p1_24 (conj (p2p1_227 Velpq Vepab Vepde Velns) (p2p1_236 Velpq Vepab Vepde Velns Velor)))))). Qed. Lemma p2p1_238: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(ep g i)->(ep i g). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Vepgi:(ep g i))=>((psym g i) Vepgi)). Qed. Lemma p2p1_239: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(ep g i)->(exists A:dom,(pl c A)/\(pl f A)). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Vepgi:(ep g i))=>((line c f) (conj p2p1_32 p2p1_34))). Qed. Lemma p2p1_241: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(ep g i)->forall C0:dom,(pl c C0)->(pl f C0)->(exists A:dom,(pl c A)/\(pl h A)). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Vepgi:(ep g i))(C0:dom)(VplcC0:(pl c C0))(VplfC0:(pl f C0))=>((line c h) (conj p2p1_32 p2p1_36))). Qed. Lemma p2p1_243: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(ep g i)->forall C0:dom,(pl c C0)->(pl f C0)->forall C1:dom,(pl c C1)->(pl h C1)->(exists A:dom,(pl f A)/\(pl h A)). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Vepgi:(ep g i))(C0:dom)(VplcC0:(pl c C0))(VplfC0:(pl f C0))(C1:dom)(VplcC1:(pl c C1))(VplhC1:(pl h C1))=>((line f h) (conj p2p1_34 p2p1_36))). Qed. Lemma p2p1_245: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(ep g i)->forall C0:dom,(pl c C0)->(pl f C0)->forall C1:dom,(pl c C1)->(pl h C1)->forall C2:dom,(pl f C2)->(pl h C2)->(exists A:dom,(pl g A)/\(pl h A)). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Vepgi:(ep g i))(C0:dom)(VplcC0:(pl c C0))(VplfC0:(pl f C0))(C1:dom)(VplcC1:(pl c C1))(VplhC1:(pl h C1))(C2:dom)(VplfC2:(pl f C2))(VplhC2:(pl h C2))=>((line g h) (conj p2p1_35 p2p1_36))). Qed. Lemma p2p1_247: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(ep g i)->forall C0:dom,(pl c C0)->(pl f C0)->forall C1:dom,(pl c C1)->(pl h C1)->forall C2:dom,(pl f C2)->(pl h C2)->forall C3:dom,(pl g C3)->(pl h C3)->(pl i C3). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Vepgi:(ep g i))(C0:dom)(VplcC0:(pl c C0))(VplfC0:(pl f C0))(C1:dom)(VplcC1:(pl c C1))(VplhC1:(pl h C1))(C2:dom)(VplfC2:(pl f C2))(VplhC2:(pl h C2))(C3:dom)(VplgC3:(pl g C3))(VplhC3:(pl h C3))=>((pcon i g C3) (conj (p2p1_238 Velpq Vepab Vepde Velns Velor Vepgi) VplgC3))). Qed. Lemma p2p1_248: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(ep g i)->forall C0:dom,(pl c C0)->(pl f C0)->forall C1:dom,(pl c C1)->(pl h C1)->forall C2:dom,(pl f C2)->(pl h C2)->forall C3:dom,(pl g C3)->(pl h C3)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Vepgi:(ep g i))(C0:dom)(VplcC0:(pl c C0))(VplfC0:(pl f C0))(C1:dom)(VplcC1:(pl c C1))(VplhC1:(pl h C1))(C2:dom)(VplfC2:(pl f C2))(VplhC2:(pl h C2))(C3:dom)(VplgC3:(pl g C3))(VplhC3:(pl h C3))=>((goal4 C3) (conj VplgC3 (conj VplhC3 (p2p1_247 Velpq Vepab Vepde Velns Velor Vepgi C0 VplcC0 VplfC0 C1 VplcC1 VplhC1 C2 VplfC2 VplhC2 C3 VplgC3 VplhC3))))). Qed. Lemma p2p1_249: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(ep g i)->forall C0:dom,(pl c C0)->(pl f C0)->forall C1:dom,(pl c C1)->(pl h C1)->forall C2:dom,(pl f C2)->(pl h C2)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Vepgi:(ep g i))(C0:dom)(VplcC0:(pl c C0))(VplfC0:(pl f C0))(C1:dom)(VplcC1:(pl c C1))(VplhC1:(pl h C1))(C2:dom)(VplfC2:(pl f C2))(VplhC2:(pl h C2))=>((ex_ind (P:=fun C3:dom=>(pl g C3)/\(pl h C3))(fun C3:dom=>(and_ind (p2p1_248 Velpq Vepab Vepde Velns Velor Vepgi C0 VplcC0 VplfC0 C1 VplcC1 VplhC1 C2 VplfC2 VplhC2 C3))))(p2p1_245 Velpq Vepab Vepde Velns Velor Vepgi C0 VplcC0 VplfC0 C1 VplcC1 VplhC1 C2 VplfC2 VplhC2))). Qed. Lemma p2p1_250: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(ep g i)->forall C0:dom,(pl c C0)->(pl f C0)->forall C1:dom,(pl c C1)->(pl h C1)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Vepgi:(ep g i))(C0:dom)(VplcC0:(pl c C0))(VplfC0:(pl f C0))(C1:dom)(VplcC1:(pl c C1))(VplhC1:(pl h C1))=>((ex_ind (P:=fun C2:dom=>(pl f C2)/\(pl h C2))(fun C2:dom=>(and_ind (p2p1_249 Velpq Vepab Vepde Velns Velor Vepgi C0 VplcC0 VplfC0 C1 VplcC1 VplhC1 C2))))(p2p1_243 Velpq Vepab Vepde Velns Velor Vepgi C0 VplcC0 VplfC0 C1 VplcC1 VplhC1))). Qed. Lemma p2p1_251: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(ep g i)->forall C0:dom,(pl c C0)->(pl f C0)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Vepgi:(ep g i))(C0:dom)(VplcC0:(pl c C0))(VplfC0:(pl f C0))=>((ex_ind (P:=fun C1:dom=>(pl c C1)/\(pl h C1))(fun C1:dom=>(and_ind (p2p1_250 Velpq Vepab Vepde Velns Velor Vepgi C0 VplcC0 VplfC0 C1))))(p2p1_241 Velpq Vepab Vepde Velns Velor Vepgi C0 VplcC0 VplfC0))). Qed. Lemma p2p1_252: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(ep g i)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Vepgi:(ep g i))=>((ex_ind (P:=fun C0:dom=>(pl c C0)/\(pl f C0))(fun C0:dom=>(and_ind (p2p1_251 Velpq Vepab Vepde Velns Velor Vepgi C0))))(p2p1_239 Velpq Vepab Vepde Velns Velor Vepgi))). Qed. Lemma p2p1_253: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(el o n). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))=>((lsym n o) Velno)). Qed. Lemma p2p1_254: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(el s o). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))=>((ltra s n o) (conj (p2p1_225 Velpq Vepab Vepde Velns) Velno))). Qed. Lemma p2p1_255: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(el o s). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))=>((lsym s o) (p2p1_254 Velpq Vepab Vepde Velns Velor Velno))). Qed. Lemma p2p1_256: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(el r n). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))=>((ltra r o n) (conj (p2p1_234 Velpq Vepab Vepde Velns Velor) (p2p1_253 Velpq Vepab Vepde Velns Velor Velno)))). Qed. Lemma p2p1_257: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(el n r). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))=>((lsym r n) (p2p1_256 Velpq Vepab Vepde Velns Velor Velno))). Qed. Lemma p2p1_265: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(pl c s). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))=>((lcon c o s) (conj p2p1_8 (p2p1_255 Velpq Vepab Vepde Velns Velor Velno)))). Qed. Lemma p2p1_267: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(pl f r). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))=>((lcon f n r) (conj p2p1_15 (p2p1_257 Velpq Vepab Vepde Velns Velor Velno)))). Qed. Lemma p2p1_272: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c) \/ (el l s). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))=>((unique l s a c) (conj p2p1_5 (conj p2p1_12 (conj p2p1_21 (p2p1_265 Velpq Vepab Vepde Velns Velor Velno)))))). Qed. Lemma p2p1_278: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(ep d f) \/ (el m r). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))=>((unique m r d f) (conj p2p1_6 (conj p2p1_19 (conj p2p1_22 (p2p1_267 Velpq Vepab Vepde Velns Velor Velno)))))). Qed. Lemma p2p1_279: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(ep d f)->(ep f d). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Vepdf:(ep d f))=>((psym d f) Vepdf)). Qed. Lemma p2p1_282: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(ep d f)->(pl f p). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Vepdf:(ep d f))=>((pcon f d p) (conj (p2p1_279 Velpq Vepab Vepde Velns Velor Velno Vepac Vepdf) p2p1_17))). Qed. Lemma p2p1_284: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(ep d f)->(ep b f) \/ (el n p). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Vepdf:(ep d f))=>((unique n p b f) (conj p2p1_7 (conj p2p1_9 (conj p2p1_15 (p2p1_282 Velpq Vepab Vepde Velns Velor Velno Vepac Vepdf)))))). Qed. Lemma p2p1_302: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(ep d f)->(ep b f)->(pl b m). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Vepdf:(ep d f))(Vepbf:(ep b f))=>((pcon b f m) (conj Vepbf p2p1_22))). Qed. Lemma p2p1_303: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(ep d f)->(ep b f)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Vepdf:(ep d f))(Vepbf:(ep b f))=>(goalbm (p2p1_302 Velpq Vepab Vepde Velns Velor Velno Vepac Vepdf Vepbf))). Qed. Lemma p2p1_304: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(ep d f)->(el n p)->(el p n). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))=>((lsym n p) Velnp)). Qed. Lemma p2p1_321: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(ep d f)->(el n p)->(pl h n). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))=>((lcon h p n) (conj p2p1_25 (p2p1_304 Velpq Vepab Vepde Velns Velor Velno Vepac Vepdf Velnp)))). Qed. Lemma p2p1_322: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(ep d f)->(el n p)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))=>((goal4 n) (conj p2p1_23 (conj (p2p1_321 Velpq Vepab Vepde Velns Velor Velno Vepac Vepdf Velnp) (p2p1_227 Velpq Vepab Vepde Velns))))). Qed. Lemma p2p1_323: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(ep d f)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Vepdf:(ep d f))=>((or_ind ((p2p1_303 Velpq Vepab Vepde Velns Velor Velno Vepac Vepdf))((p2p1_322 Velpq Vepab Vepde Velns Velor Velno Vepac Vepdf)))(p2p1_284 Velpq Vepab Vepde Velns Velor Velno Vepac Vepdf))). Qed. Lemma p2p1_324: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(el m r)->(el r m). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Velmr:(el m r))=>((lsym m r) Velmr)). Qed. Lemma p2p1_325: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(el m r)->(el o m). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Velmr:(el m r))=>((ltra o r m) (conj Velor (p2p1_324 Velpq Vepab Vepde Velns Velor Velno Vepac Velmr)))). Qed. Lemma p2p1_327: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(el m r)->(el n m). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Velmr:(el m r))=>((ltra n o m) (conj Velno (p2p1_325 Velpq Vepab Vepde Velns Velor Velno Vepac Velmr)))). Qed. Lemma p2p1_331: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(el m r)->(pl b m). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Velmr:(el m r))=>((lcon b n m) (conj p2p1_7 (p2p1_327 Velpq Vepab Vepde Velns Velor Velno Vepac Velmr)))). Qed. Lemma p2p1_332: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->(el m r)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))(Velmr:(el m r))=>(goalbm (p2p1_331 Velpq Vepab Vepde Velns Velor Velno Vepac Velmr))). Qed. Lemma p2p1_333: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(ep a c)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vepac:(ep a c))=>((or_ind ((p2p1_323 Velpq Vepab Vepde Velns Velor Velno Vepac))((p2p1_332 Velpq Vepab Vepde Velns Velor Velno Vepac)))(p2p1_278 Velpq Vepab Vepde Velns Velor Velno Vepac))). Qed. Lemma p2p1_334: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(el l s)->(el s l). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vells:(el l s))=>((lsym l s) Vells)). Qed. Lemma p2p1_335: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(el l s)->(el n l). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vells:(el l s))=>((ltra n s l) (conj Velns (p2p1_334 Velpq Vepab Vepde Velns Velor Velno Vells)))). Qed. Lemma p2p1_341: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(el l s)->(pl f l). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vells:(el l s))=>((lcon f n l) (conj p2p1_15 (p2p1_335 Velpq Vepab Vepde Velns Velor Velno Vells)))). Qed. Lemma p2p1_342: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->(el l s)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))(Vells:(el l s))=>(goalfl (p2p1_341 Velpq Vepab Vepde Velns Velor Velno Vells))). Qed. Lemma p2p1_343: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->(el n o)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))(Velno:(el n o))=>((or_ind ((p2p1_333 Velpq Vepab Vepde Velns Velor Velno))((p2p1_342 Velpq Vepab Vepde Velns Velor Velno)))(p2p1_272 Velpq Vepab Vepde Velns Velor Velno))). Qed. Lemma p2p1_344: (el p q)->(ep a b)->(ep d e)->(el n s)->(el o r)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))(Velor:(el o r))=>((or_ind ((p2p1_252 Velpq Vepab Vepde Velns Velor))((p2p1_343 Velpq Vepab Vepde Velns Velor)))(p2p1_237 Velpq Vepab Vepde Velns Velor))). Qed. Lemma p2p1_345: (el p q)->(ep a b)->(ep d e)->(el n s)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))=>((or_ind ((p2p1_233 Velpq Vepab Vepde Velns))((p2p1_344 Velpq Vepab Vepde Velns)))(p2p1_228 Velpq Vepab Vepde Velns))). Qed. Lemma p2p1_346: (el p q)->(ep a b)->(ep d e)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Vepde:(ep d e))=>((or_ind ((p2p1_224 Velpq Vepab Vepde))((p2p1_345 Velpq Vepab Vepde)))(p2p1_219 Velpq Vepab Vepde))). Qed. Lemma p2p1_347: (el p q)->(ep a b)->(el m p)->(el p m). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Velmp:(el m p))=>((lsym m p) Velmp)). Qed. Lemma p2p1_350: (el p q)->(ep a b)->(el m p)->(pl b m). Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Velmp:(el m p))=>((lcon b p m) (conj p2p1_9 (p2p1_347 Velpq Vepab Velmp)))). Qed. Lemma p2p1_351: (el p q)->(ep a b)->(el m p)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))(Velmp:(el m p))=>(goalbm (p2p1_350 Velpq Vepab Velmp))). Qed. Lemma p2p1_352: (el p q)->(ep a b)->goal. Proof. exact (fun (Velpq:(el p q))(Vepab:(ep a b))=>((or_ind ((p2p1_346 Velpq Vepab))((p2p1_351 Velpq Vepab)))(p2p1_215 Velpq Vepab))). Qed. Lemma p2p1_353: (el p q)->(el l q)->(el q l). Proof. exact (fun (Velpq:(el p q))(Vellq:(el l q))=>((lsym l q) Vellq)). Qed. Lemma p2p1_354: (el p q)->(el l q)->(el p l). Proof. exact (fun (Velpq:(el p q))(Vellq:(el l q))=>((ltra p q l) (conj Velpq (p2p1_353 Velpq Vellq)))). Qed. Lemma p2p1_356: (el p q)->(el l q)->(pl d l). Proof. exact (fun (Velpq:(el p q))(Vellq:(el l q))=>((lcon d p l) (conj p2p1_17 (p2p1_354 Velpq Vellq)))). Qed. Lemma p2p1_357: (el p q)->(el l q)->goal. Proof. exact (fun (Velpq:(el p q))(Vellq:(el l q))=>(goaldl (p2p1_356 Velpq Vellq))). Qed. Lemma p2p1_358: (el p q)->goal. Proof. exact (fun (Velpq:(el p q))=>((or_ind ((p2p1_352 Velpq))((p2p1_357 Velpq)))(p2p1_211 Velpq))). Qed. Lemma p2p1_359: (el r s)->(el s r). Proof. exact (fun (Velrs:(el r s))=>((lsym r s) Velrs)). Qed. Lemma p2p1_360: (el r s)->(pl c s). Proof. exact (fun (Velrs:(el r s))=>((lcon c r s) (conj p2p1_11 Velrs))). Qed. Lemma p2p1_363: (el r s)->(pl f r). Proof. exact (fun (Velrs:(el r s))=>((lcon f s r) (conj p2p1_20 (p2p1_359 Velrs)))). Qed. Lemma p2p1_364: (el r s)->(ep a c) \/ (el l s). Proof. exact (fun (Velrs:(el r s))=>((unique l s a c) (conj p2p1_5 (conj p2p1_12 (conj p2p1_21 (p2p1_360 Velrs)))))). Qed. Lemma p2p1_365: (el r s)->(ep a c)->(ep c a). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))=>((psym a c) Vepac)). Qed. Lemma p2p1_367: (el r s)->(ep a c)->(pl c q). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))=>((pcon c a q) (conj (p2p1_365 Velrs Vepac) p2p1_10))). Qed. Lemma p2p1_368: (el r s)->(ep a c)->(ep d f) \/ (el m r). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))=>((unique m r d f) (conj p2p1_6 (conj p2p1_19 (conj p2p1_22 (p2p1_363 Velrs)))))). Qed. Lemma p2p1_369: (el r s)->(ep a c)->(ep d f)->(ep f d). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))=>((psym d f) Vepdf)). Qed. Lemma p2p1_371: (el r s)->(ep a c)->(ep d f)->(pl f p). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))=>((pcon f d p) (conj (p2p1_369 Velrs Vepac Vepdf) p2p1_17))). Qed. Lemma p2p1_372: (el r s)->(ep a c)->(ep d f)->(ep b f) \/ (el n p). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))=>((unique n p b f) (conj p2p1_7 (conj p2p1_9 (conj p2p1_15 (p2p1_371 Velrs Vepac Vepdf)))))). Qed. Lemma p2p1_377: (el r s)->(ep a c)->(ep d f)->(ep b f)->(pl b m). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Vepbf:(ep b f))=>((pcon b f m) (conj Vepbf p2p1_22))). Qed. Lemma p2p1_378: (el r s)->(ep a c)->(ep d f)->(ep b f)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Vepbf:(ep b f))=>(goalbm (p2p1_377 Velrs Vepac Vepdf Vepbf))). Qed. Lemma p2p1_379: (el r s)->(ep a c)->(ep d f)->(el n p)->(el p n). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))=>((lsym n p) Velnp)). Qed. Lemma p2p1_381: (el r s)->(ep a c)->(ep d f)->(el n p)->(pl h n). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))=>((lcon h p n) (conj p2p1_25 (p2p1_379 Velrs Vepac Vepdf Velnp)))). Qed. Lemma p2p1_382: (el r s)->(ep a c)->(ep d f)->(el n p)->(ep c e) \/ (el o q). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))=>((unique o q c e) (conj p2p1_8 (conj (p2p1_367 Velrs Vepac) (conj p2p1_16 p2p1_18))))). Qed. Lemma p2p1_386: (el r s)->(ep a c)->(ep d f)->(el n p)->(ep c e)->(pl c m). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Vepce:(ep c e))=>((pcon c e m) (conj Vepce p2p1_14))). Qed. Lemma p2p1_387: (el r s)->(ep a c)->(ep d f)->(el n p)->(ep c e)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Vepce:(ep c e))=>(goalcm (p2p1_386 Velrs Vepac Vepdf Velnp Vepce))). Qed. Lemma p2p1_388: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el q o). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))=>((lsym o q) Veloq)). Qed. Lemma p2p1_390: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(pl h o). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))=>((lcon h q o) (conj p2p1_26 (p2p1_388 Velrs Vepac Vepdf Velnp Veloq)))). Qed. Lemma p2p1_391: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(ep g h) \/ (el n o). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))=>((unique n o g h) (conj p2p1_23 (conj p2p1_24 (conj (p2p1_381 Velrs Vepac Vepdf Velnp) (p2p1_390 Velrs Vepac Vepdf Velnp Veloq)))))). Qed. Lemma p2p1_392: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(ep g h)->(ep h g). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Vepgh:(ep g h))=>((psym g h) Vepgh)). Qed. Lemma p2p1_393: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(ep g h)->(exists A:dom,(pl b A)/\(pl e A)). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Vepgh:(ep g h))=>((line b e) (conj p2p1_31 p2p1_33))). Qed. Lemma p2p1_395: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(ep g h)->forall C0:dom,(pl b C0)->(pl e C0)->(exists A:dom,(pl b A)/\(pl i A)). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Vepgh:(ep g h))(C0:dom)(VplbC0:(pl b C0))(VpleC0:(pl e C0))=>((line b i) (conj p2p1_31 p2p1_37))). Qed. Lemma p2p1_397: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(ep g h)->forall C0:dom,(pl b C0)->(pl e C0)->forall C1:dom,(pl b C1)->(pl i C1)->(exists A:dom,(pl e A)/\(pl i A)). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Vepgh:(ep g h))(C0:dom)(VplbC0:(pl b C0))(VpleC0:(pl e C0))(C1:dom)(VplbC1:(pl b C1))(VpliC1:(pl i C1))=>((line e i) (conj p2p1_33 p2p1_37))). Qed. Lemma p2p1_399: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(ep g h)->forall C0:dom,(pl b C0)->(pl e C0)->forall C1:dom,(pl b C1)->(pl i C1)->forall C2:dom,(pl e C2)->(pl i C2)->(exists A:dom,(pl g A)/\(pl i A)). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Vepgh:(ep g h))(C0:dom)(VplbC0:(pl b C0))(VpleC0:(pl e C0))(C1:dom)(VplbC1:(pl b C1))(VpliC1:(pl i C1))(C2:dom)(VpleC2:(pl e C2))(VpliC2:(pl i C2))=>((line g i) (conj p2p1_35 p2p1_37))). Qed. Lemma p2p1_401: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(ep g h)->forall C0:dom,(pl b C0)->(pl e C0)->forall C1:dom,(pl b C1)->(pl i C1)->forall C2:dom,(pl e C2)->(pl i C2)->forall C3:dom,(pl g C3)->(pl i C3)->(pl h C3). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Vepgh:(ep g h))(C0:dom)(VplbC0:(pl b C0))(VpleC0:(pl e C0))(C1:dom)(VplbC1:(pl b C1))(VpliC1:(pl i C1))(C2:dom)(VpleC2:(pl e C2))(VpliC2:(pl i C2))(C3:dom)(VplgC3:(pl g C3))(VpliC3:(pl i C3))=>((pcon h g C3) (conj (p2p1_392 Velrs Vepac Vepdf Velnp Veloq Vepgh) VplgC3))). Qed. Lemma p2p1_402: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(ep g h)->forall C0:dom,(pl b C0)->(pl e C0)->forall C1:dom,(pl b C1)->(pl i C1)->forall C2:dom,(pl e C2)->(pl i C2)->forall C3:dom,(pl g C3)->(pl i C3)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Vepgh:(ep g h))(C0:dom)(VplbC0:(pl b C0))(VpleC0:(pl e C0))(C1:dom)(VplbC1:(pl b C1))(VpliC1:(pl i C1))(C2:dom)(VpleC2:(pl e C2))(VpliC2:(pl i C2))(C3:dom)(VplgC3:(pl g C3))(VpliC3:(pl i C3))=>((goal4 C3) (conj VplgC3 (conj (p2p1_401 Velrs Vepac Vepdf Velnp Veloq Vepgh C0 VplbC0 VpleC0 C1 VplbC1 VpliC1 C2 VpleC2 VpliC2 C3 VplgC3 VpliC3) VpliC3)))). Qed. Lemma p2p1_403: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(ep g h)->forall C0:dom,(pl b C0)->(pl e C0)->forall C1:dom,(pl b C1)->(pl i C1)->forall C2:dom,(pl e C2)->(pl i C2)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Vepgh:(ep g h))(C0:dom)(VplbC0:(pl b C0))(VpleC0:(pl e C0))(C1:dom)(VplbC1:(pl b C1))(VpliC1:(pl i C1))(C2:dom)(VpleC2:(pl e C2))(VpliC2:(pl i C2))=>((ex_ind (P:=fun C3:dom=>(pl g C3)/\(pl i C3))(fun C3:dom=>(and_ind (p2p1_402 Velrs Vepac Vepdf Velnp Veloq Vepgh C0 VplbC0 VpleC0 C1 VplbC1 VpliC1 C2 VpleC2 VpliC2 C3))))(p2p1_399 Velrs Vepac Vepdf Velnp Veloq Vepgh C0 VplbC0 VpleC0 C1 VplbC1 VpliC1 C2 VpleC2 VpliC2))). Qed. Lemma p2p1_404: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(ep g h)->forall C0:dom,(pl b C0)->(pl e C0)->forall C1:dom,(pl b C1)->(pl i C1)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Vepgh:(ep g h))(C0:dom)(VplbC0:(pl b C0))(VpleC0:(pl e C0))(C1:dom)(VplbC1:(pl b C1))(VpliC1:(pl i C1))=>((ex_ind (P:=fun C2:dom=>(pl e C2)/\(pl i C2))(fun C2:dom=>(and_ind (p2p1_403 Velrs Vepac Vepdf Velnp Veloq Vepgh C0 VplbC0 VpleC0 C1 VplbC1 VpliC1 C2))))(p2p1_397 Velrs Vepac Vepdf Velnp Veloq Vepgh C0 VplbC0 VpleC0 C1 VplbC1 VpliC1))). Qed. Lemma p2p1_405: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(ep g h)->forall C0:dom,(pl b C0)->(pl e C0)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Vepgh:(ep g h))(C0:dom)(VplbC0:(pl b C0))(VpleC0:(pl e C0))=>((ex_ind (P:=fun C1:dom=>(pl b C1)/\(pl i C1))(fun C1:dom=>(and_ind (p2p1_404 Velrs Vepac Vepdf Velnp Veloq Vepgh C0 VplbC0 VpleC0 C1))))(p2p1_395 Velrs Vepac Vepdf Velnp Veloq Vepgh C0 VplbC0 VpleC0))). Qed. Lemma p2p1_406: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(ep g h)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Vepgh:(ep g h))=>((ex_ind (P:=fun C0:dom=>(pl b C0)/\(pl e C0))(fun C0:dom=>(and_ind (p2p1_405 Velrs Vepac Vepdf Velnp Veloq Vepgh C0))))(p2p1_393 Velrs Vepac Vepdf Velnp Veloq Vepgh))). Qed. Lemma p2p1_407: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(el o n). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))=>((lsym n o) Velno)). Qed. Lemma p2p1_408: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(el p o). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))=>((ltra p n o) (conj (p2p1_379 Velrs Vepac Vepdf Velnp) Velno))). Qed. Lemma p2p1_409: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(el o p). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))=>((lsym p o) (p2p1_408 Velrs Vepac Vepdf Velnp Veloq Velno))). Qed. Lemma p2p1_410: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(el q n). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))=>((ltra q o n) (conj (p2p1_388 Velrs Vepac Vepdf Velnp Veloq) (p2p1_407 Velrs Vepac Vepdf Velnp Veloq Velno)))). Qed. Lemma p2p1_411: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(el n q). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))=>((lsym q n) (p2p1_410 Velrs Vepac Vepdf Velnp Veloq Velno))). Qed. Lemma p2p1_415: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(pl b q). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))=>((lcon b n q) (conj p2p1_7 (p2p1_411 Velrs Vepac Vepdf Velnp Veloq Velno)))). Qed. Lemma p2p1_425: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(pl e p). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))=>((lcon e o p) (conj p2p1_16 (p2p1_409 Velrs Vepac Vepdf Velnp Veloq Velno)))). Qed. Lemma p2p1_426: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b) \/ (el l q). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))=>((unique l q a b) (conj p2p1_5 (conj p2p1_10 (conj p2p1_13 (p2p1_415 Velrs Vepac Vepdf Velnp Veloq Velno)))))). Qed. Lemma p2p1_427: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(ep b a). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))=>((psym a b) Vepab)). Qed. Lemma p2p1_430: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(pl b s). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))=>((pcon b a s) (conj (p2p1_427 Velrs Vepac Vepdf Velnp Veloq Velno Vepab) p2p1_12))). Qed. Lemma p2p1_432: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(ep d e) \/ (el m p). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))=>((unique m p d e) (conj p2p1_6 (conj p2p1_17 (conj p2p1_14 (p2p1_425 Velrs Vepac Vepdf Velnp Veloq Velno)))))). Qed. Lemma p2p1_438: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(ep d e)->(ep b f) \/ (el n s). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))(Vepde:(ep d e))=>((unique n s b f) (conj p2p1_7 (conj (p2p1_430 Velrs Vepac Vepdf Velnp Veloq Velno Vepab) (conj p2p1_15 p2p1_20))))). Qed. Lemma p2p1_456: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(ep d e)->(ep b f)->(pl b m). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))(Vepde:(ep d e))(Vepbf:(ep b f))=>((pcon b f m) (conj Vepbf p2p1_22))). Qed. Lemma p2p1_457: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(ep d e)->(ep b f)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))(Vepde:(ep d e))(Vepbf:(ep b f))=>(goalbm (p2p1_456 Velrs Vepac Vepdf Velnp Veloq Velno Vepab Vepde Vepbf))). Qed. Lemma p2p1_461: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(ep d e)->(el n s)->(el p s). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))=>((ltra p n s) (conj (p2p1_379 Velrs Vepac Vepdf Velnp) Velns))). Qed. Lemma p2p1_473: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(ep d e)->(el n s)->(pl g s). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))=>((lcon g n s) (conj p2p1_23 Velns))). Qed. Lemma p2p1_475: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(ep d e)->(el n s)->(pl h s). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))=>((lcon h p s) (conj p2p1_25 (p2p1_461 Velrs Vepac Vepdf Velnp Veloq Velno Vepab Vepde Velns)))). Qed. Lemma p2p1_476: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(ep d e)->(el n s)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))(Vepde:(ep d e))(Velns:(el n s))=>((goal4 s) (conj (p2p1_473 Velrs Vepac Vepdf Velnp Veloq Velno Vepab Vepde Velns) (conj (p2p1_475 Velrs Vepac Vepdf Velnp Veloq Velno Vepab Vepde Velns) p2p1_28)))). Qed. Lemma p2p1_477: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(ep d e)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))(Vepde:(ep d e))=>((or_ind ((p2p1_457 Velrs Vepac Vepdf Velnp Veloq Velno Vepab Vepde))((p2p1_476 Velrs Vepac Vepdf Velnp Veloq Velno Vepab Vepde)))(p2p1_438 Velrs Vepac Vepdf Velnp Veloq Velno Vepab Vepde))). Qed. Lemma p2p1_478: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(el m p)->(el p m). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))(Velmp:(el m p))=>((lsym m p) Velmp)). Qed. Lemma p2p1_479: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(el m p)->(el n m). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))(Velmp:(el m p))=>((ltra n p m) (conj Velnp (p2p1_478 Velrs Vepac Vepdf Velnp Veloq Velno Vepab Velmp)))). Qed. Lemma p2p1_485: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(el m p)->(pl b m). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))(Velmp:(el m p))=>((lcon b n m) (conj p2p1_7 (p2p1_479 Velrs Vepac Vepdf Velnp Veloq Velno Vepab Velmp)))). Qed. Lemma p2p1_486: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->(el m p)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))(Velmp:(el m p))=>(goalbm (p2p1_485 Velrs Vepac Vepdf Velnp Veloq Velno Vepab Velmp))). Qed. Lemma p2p1_487: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(ep a b)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vepab:(ep a b))=>((or_ind ((p2p1_477 Velrs Vepac Vepdf Velnp Veloq Velno Vepab))((p2p1_486 Velrs Vepac Vepdf Velnp Veloq Velno Vepab)))(p2p1_432 Velrs Vepac Vepdf Velnp Veloq Velno Vepab))). Qed. Lemma p2p1_488: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(el l q)->(el q l). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vellq:(el l q))=>((lsym l q) Vellq)). Qed. Lemma p2p1_489: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(el l q)->(el o l). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vellq:(el l q))=>((ltra o q l) (conj Veloq (p2p1_488 Velrs Vepac Vepdf Velnp Veloq Velno Vellq)))). Qed. Lemma p2p1_491: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(el l q)->(el n l). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vellq:(el l q))=>((ltra n o l) (conj Velno (p2p1_489 Velrs Vepac Vepdf Velnp Veloq Velno Vellq)))). Qed. Lemma p2p1_495: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(el l q)->(pl f l). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vellq:(el l q))=>((lcon f n l) (conj p2p1_15 (p2p1_491 Velrs Vepac Vepdf Velnp Veloq Velno Vellq)))). Qed. Lemma p2p1_496: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->(el l q)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))(Vellq:(el l q))=>(goalfl (p2p1_495 Velrs Vepac Vepdf Velnp Veloq Velno Vellq))). Qed. Lemma p2p1_497: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->(el n o)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))(Velno:(el n o))=>((or_ind ((p2p1_487 Velrs Vepac Vepdf Velnp Veloq Velno))((p2p1_496 Velrs Vepac Vepdf Velnp Veloq Velno)))(p2p1_426 Velrs Vepac Vepdf Velnp Veloq Velno))). Qed. Lemma p2p1_498: (el r s)->(ep a c)->(ep d f)->(el n p)->(el o q)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))(Veloq:(el o q))=>((or_ind ((p2p1_406 Velrs Vepac Vepdf Velnp Veloq))((p2p1_497 Velrs Vepac Vepdf Velnp Veloq)))(p2p1_391 Velrs Vepac Vepdf Velnp Veloq))). Qed. Lemma p2p1_499: (el r s)->(ep a c)->(ep d f)->(el n p)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))(Velnp:(el n p))=>((or_ind ((p2p1_387 Velrs Vepac Vepdf Velnp))((p2p1_498 Velrs Vepac Vepdf Velnp)))(p2p1_382 Velrs Vepac Vepdf Velnp))). Qed. Lemma p2p1_500: (el r s)->(ep a c)->(ep d f)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Vepdf:(ep d f))=>((or_ind ((p2p1_378 Velrs Vepac Vepdf))((p2p1_499 Velrs Vepac Vepdf)))(p2p1_372 Velrs Vepac Vepdf))). Qed. Lemma p2p1_501: (el r s)->(ep a c)->(el m r)->(el r m). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Velmr:(el m r))=>((lsym m r) Velmr)). Qed. Lemma p2p1_504: (el r s)->(ep a c)->(el m r)->(pl c m). Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Velmr:(el m r))=>((lcon c r m) (conj p2p1_11 (p2p1_501 Velrs Vepac Velmr)))). Qed. Lemma p2p1_505: (el r s)->(ep a c)->(el m r)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))(Velmr:(el m r))=>(goalcm (p2p1_504 Velrs Vepac Velmr))). Qed. Lemma p2p1_506: (el r s)->(ep a c)->goal. Proof. exact (fun (Velrs:(el r s))(Vepac:(ep a c))=>((or_ind ((p2p1_500 Velrs Vepac))((p2p1_505 Velrs Vepac)))(p2p1_368 Velrs Vepac))). Qed. Lemma p2p1_507: (el r s)->(el l s)->(el s l). Proof. exact (fun (Velrs:(el r s))(Vells:(el l s))=>((lsym l s) Vells)). Qed. Lemma p2p1_508: (el r s)->(el l s)->(el r l). Proof. exact (fun (Velrs:(el r s))(Vells:(el l s))=>((ltra r s l) (conj Velrs (p2p1_507 Velrs Vells)))). Qed. Lemma p2p1_512: (el r s)->(el l s)->(pl d l). Proof. exact (fun (Velrs:(el r s))(Vells:(el l s))=>((lcon d r l) (conj p2p1_19 (p2p1_508 Velrs Vells)))). Qed. Lemma p2p1_513: (el r s)->(el l s)->goal. Proof. exact (fun (Velrs:(el r s))(Vells:(el l s))=>(goaldl (p2p1_512 Velrs Vells))). Qed. Lemma p2p1_514: (el r s)->goal. Proof. exact (fun (Velrs:(el r s))=>((or_ind ((p2p1_506 Velrs))((p2p1_513 Velrs)))(p2p1_364 Velrs))). Qed. Lemma p2p1_515: goal. Proof. exact (((or_ind (ex_ind (P:=fun C0:dom=>(col g h i C0))(fun C0:dom=>((p2p1_50 C0))))(or_ind (p2p1_205)(or_ind (p2p1_358)(p2p1_514))))p2p1_46)). Qed. Check p2p1_515. End p2p1_.