Section nl. Let false:=False. Let false_ind:=False_ind. Variable dom:Set. Variable e:dom->dom->Prop. Variable goal:Prop. Variable r:dom->dom->Prop. Variable s:dom->dom->Prop. Variable a b c:dom. Hypothesis found:forall A:dom,(s b A)/\(s c A)->goal. Hypothesis assump:(s a b)/\(s a c). Hypothesis ref_e:forall A:dom,(e A A). Hypothesis sym_e:forall A B:dom,(e A B)->(e B A). Hypothesis e_in_s:forall A B:dom,(e A B)->(s A B). Hypothesis r_in_s:forall A B:dom,(r A B)->(s A B). Hypothesis trans_s:forall A B C:dom,(s A B)/\(s B C)->(s A C). Hypothesis lo_cfl:forall A B C:dom,(r A B)/\(r A C)->(exists D:dom,(s B D)/\(s C D)). Hypothesis ih_cfl:forall A B C:dom,(r a A)/\(s A B)/\(s A C)->(exists D:dom,(s B D)/\(s C D)). Hypothesis e_or_rs:forall A B:dom,(s A B)->(e A B) \/ (exists C:dom,(r A C)/\(s C B)). Lemma nl1: (s a b)/\(s a c). Proof. exact (assump). Qed. Lemma nl3: (e b b). Proof. exact ((ref_e b)). Qed. Lemma nl4: (e c c). Proof. exact ((ref_e c)). Qed. Lemma nl6: (s b b). Proof. exact (((e_in_s b b) nl3)). Qed. Lemma nl7: (s c c). Proof. exact (((e_in_s c c) nl4)). Qed. Lemma nl8: (e a b) \/ (exists A:dom,(r a A)/\(s A b)). Proof. exact (((e_or_rs a b) (proj1 nl1))). Qed. Lemma nl9: (e a b)->(e b a). Proof. exact (fun (Veab:(e a b))=>((sym_e a b) Veab)). Qed. Lemma nl10: (e a b)->(s b a). Proof. exact (fun (Veab:(e a b))=>((e_in_s b a) (nl9 Veab))). Qed. Lemma nl11: (e a b)->(s b c). Proof. exact (fun (Veab:(e a b))=>((trans_s b a c) (conj (nl10 Veab) (proj2 nl1)))). Qed. Lemma nl12: (e a b)->goal. Proof. exact (fun (Veab:(e a b))=>((found c) (conj (nl11 Veab) nl7))). Qed. Lemma nl16: forall C0:dom,(r a C0)->(s C0 b)->(e a c) \/ (exists A:dom,(r a A)/\(s A c)). Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))=>((e_or_rs a c) (proj2 nl1))). Qed. Lemma nl17: forall C0:dom,(r a C0)->(s C0 b)->(e a c)->(e c a). Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(Veac:(e a c))=>((sym_e a c) Veac)). Qed. Lemma nl18: forall C0:dom,(r a C0)->(s C0 b)->(e a c)->(s c a). Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(Veac:(e a c))=>((e_in_s c a) (nl17 C0 VraC0 VsC0b Veac))). Qed. Lemma nl19: forall C0:dom,(r a C0)->(s C0 b)->(e a c)->(s c b). Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(Veac:(e a c))=>((trans_s c a b) (conj (nl18 C0 VraC0 VsC0b Veac) (proj1 nl1)))). Qed. Lemma nl20: forall C0:dom,(r a C0)->(s C0 b)->(e a c)->goal. Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(Veac:(e a c))=>((found b) (conj nl6 (nl19 C0 VraC0 VsC0b Veac)))). Qed. Lemma nl24: forall C0:dom,(r a C0)->(s C0 b)->forall C1:dom,(r a C1)->(s C1 c)->(exists A:dom,(s C0 A)/\(s C1 A)). Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(C1:dom)(VraC1:(r a C1))(VsC1c:(s C1 c))=>((lo_cfl a C0 C1) (conj VraC0 VraC1))). Qed. Lemma nl28: forall C0:dom,(r a C0)->(s C0 b)->forall C1:dom,(r a C1)->(s C1 c)->forall C2:dom,(s C0 C2)->(s C1 C2)->(exists A:dom,(s b A)/\(s C2 A)). Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(C1:dom)(VraC1:(r a C1))(VsC1c:(s C1 c))(C2:dom)(VsC0C2:(s C0 C2))(VsC1C2:(s C1 C2))=>((ih_cfl C0 b C2) (conj VraC0 (conj VsC0b VsC0C2)))). Qed. Lemma nl34: forall C0:dom,(r a C0)->(s C0 b)->forall C1:dom,(r a C1)->(s C1 c)->forall C2:dom,(s C0 C2)->(s C1 C2)->forall C3:dom,(s b C3)->(s C2 C3)->(exists A:dom,(s c A)/\(s C2 A)). Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(C1:dom)(VraC1:(r a C1))(VsC1c:(s C1 c))(C2:dom)(VsC0C2:(s C0 C2))(VsC1C2:(s C1 C2))(C3:dom)(VsbC3:(s b C3))(VsC2C3:(s C2 C3))=>((ih_cfl C1 c C2) (conj VraC1 (conj VsC1c VsC1C2)))). Qed. Lemma nl39: forall C0:dom,(r a C0)->(s C0 b)->forall C1:dom,(r a C1)->(s C1 c)->forall C2:dom,(s C0 C2)->(s C1 C2)->forall C3:dom,(s b C3)->(s C2 C3)->forall C4:dom,(s c C4)->(s C2 C4)->(s C0 C4). Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(C1:dom)(VraC1:(r a C1))(VsC1c:(s C1 c))(C2:dom)(VsC0C2:(s C0 C2))(VsC1C2:(s C1 C2))(C3:dom)(VsbC3:(s b C3))(VsC2C3:(s C2 C3))(C4:dom)(VscC4:(s c C4))(VsC2C4:(s C2 C4))=>((trans_s C0 C2 C4) (conj VsC0C2 VsC2C4))). Qed. Lemma nl40: forall C0:dom,(r a C0)->(s C0 b)->forall C1:dom,(r a C1)->(s C1 c)->forall C2:dom,(s C0 C2)->(s C1 C2)->forall C3:dom,(s b C3)->(s C2 C3)->forall C4:dom,(s c C4)->(s C2 C4)->(exists A:dom,(s b A)/\(s C4 A)). Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(C1:dom)(VraC1:(r a C1))(VsC1c:(s C1 c))(C2:dom)(VsC0C2:(s C0 C2))(VsC1C2:(s C1 C2))(C3:dom)(VsbC3:(s b C3))(VsC2C3:(s C2 C3))(C4:dom)(VscC4:(s c C4))(VsC2C4:(s C2 C4))=>((ih_cfl C0 b C4) (conj VraC0 (conj VsC0b (nl39 C0 VraC0 VsC0b C1 VraC1 VsC1c C2 VsC0C2 VsC1C2 C3 VsbC3 VsC2C3 C4 VscC4 VsC2C4))))). Qed. Lemma nl45: forall C0:dom,(r a C0)->(s C0 b)->forall C1:dom,(r a C1)->(s C1 c)->forall C2:dom,(s C0 C2)->(s C1 C2)->forall C3:dom,(s b C3)->(s C2 C3)->forall C4:dom,(s c C4)->(s C2 C4)->forall C5:dom,(s b C5)->(s C4 C5)->(s c C5). Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(C1:dom)(VraC1:(r a C1))(VsC1c:(s C1 c))(C2:dom)(VsC0C2:(s C0 C2))(VsC1C2:(s C1 C2))(C3:dom)(VsbC3:(s b C3))(VsC2C3:(s C2 C3))(C4:dom)(VscC4:(s c C4))(VsC2C4:(s C2 C4))(C5:dom)(VsbC5:(s b C5))(VsC4C5:(s C4 C5))=>((trans_s c C4 C5) (conj VscC4 VsC4C5))). Qed. Lemma nl46: forall C0:dom,(r a C0)->(s C0 b)->forall C1:dom,(r a C1)->(s C1 c)->forall C2:dom,(s C0 C2)->(s C1 C2)->forall C3:dom,(s b C3)->(s C2 C3)->forall C4:dom,(s c C4)->(s C2 C4)->forall C5:dom,(s b C5)->(s C4 C5)->goal. Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(C1:dom)(VraC1:(r a C1))(VsC1c:(s C1 c))(C2:dom)(VsC0C2:(s C0 C2))(VsC1C2:(s C1 C2))(C3:dom)(VsbC3:(s b C3))(VsC2C3:(s C2 C3))(C4:dom)(VscC4:(s c C4))(VsC2C4:(s C2 C4))(C5:dom)(VsbC5:(s b C5))(VsC4C5:(s C4 C5))=>((found C5) (conj VsbC5 (nl45 C0 VraC0 VsC0b C1 VraC1 VsC1c C2 VsC0C2 VsC1C2 C3 VsbC3 VsC2C3 C4 VscC4 VsC2C4 C5 VsbC5 VsC4C5)))). Qed. Lemma nl47: forall C0:dom,(r a C0)->(s C0 b)->forall C1:dom,(r a C1)->(s C1 c)->forall C2:dom,(s C0 C2)->(s C1 C2)->forall C3:dom,(s b C3)->(s C2 C3)->forall C4:dom,(s c C4)->(s C2 C4)->goal. Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(C1:dom)(VraC1:(r a C1))(VsC1c:(s C1 c))(C2:dom)(VsC0C2:(s C0 C2))(VsC1C2:(s C1 C2))(C3:dom)(VsbC3:(s b C3))(VsC2C3:(s C2 C3))(C4:dom)(VscC4:(s c C4))(VsC2C4:(s C2 C4))=>((ex_ind (P:=fun C5:dom=>(s b C5)/\(s C4 C5))(fun C5:dom=>(and_ind (nl46 C0 VraC0 VsC0b C1 VraC1 VsC1c C2 VsC0C2 VsC1C2 C3 VsbC3 VsC2C3 C4 VscC4 VsC2C4 C5))))(nl40 C0 VraC0 VsC0b C1 VraC1 VsC1c C2 VsC0C2 VsC1C2 C3 VsbC3 VsC2C3 C4 VscC4 VsC2C4))). Qed. Lemma nl48: forall C0:dom,(r a C0)->(s C0 b)->forall C1:dom,(r a C1)->(s C1 c)->forall C2:dom,(s C0 C2)->(s C1 C2)->forall C3:dom,(s b C3)->(s C2 C3)->goal. Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(C1:dom)(VraC1:(r a C1))(VsC1c:(s C1 c))(C2:dom)(VsC0C2:(s C0 C2))(VsC1C2:(s C1 C2))(C3:dom)(VsbC3:(s b C3))(VsC2C3:(s C2 C3))=>((ex_ind (P:=fun C4:dom=>(s c C4)/\(s C2 C4))(fun C4:dom=>(and_ind (nl47 C0 VraC0 VsC0b C1 VraC1 VsC1c C2 VsC0C2 VsC1C2 C3 VsbC3 VsC2C3 C4))))(nl34 C0 VraC0 VsC0b C1 VraC1 VsC1c C2 VsC0C2 VsC1C2 C3 VsbC3 VsC2C3))). Qed. Lemma nl49: forall C0:dom,(r a C0)->(s C0 b)->forall C1:dom,(r a C1)->(s C1 c)->forall C2:dom,(s C0 C2)->(s C1 C2)->goal. Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(C1:dom)(VraC1:(r a C1))(VsC1c:(s C1 c))(C2:dom)(VsC0C2:(s C0 C2))(VsC1C2:(s C1 C2))=>((ex_ind (P:=fun C3:dom=>(s b C3)/\(s C2 C3))(fun C3:dom=>(and_ind (nl48 C0 VraC0 VsC0b C1 VraC1 VsC1c C2 VsC0C2 VsC1C2 C3))))(nl28 C0 VraC0 VsC0b C1 VraC1 VsC1c C2 VsC0C2 VsC1C2))). Qed. Lemma nl50: forall C0:dom,(r a C0)->(s C0 b)->forall C1:dom,(r a C1)->(s C1 c)->goal. Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))(C1:dom)(VraC1:(r a C1))(VsC1c:(s C1 c))=>((ex_ind (P:=fun C2:dom=>(s C0 C2)/\(s C1 C2))(fun C2:dom=>(and_ind (nl49 C0 VraC0 VsC0b C1 VraC1 VsC1c C2))))(nl24 C0 VraC0 VsC0b C1 VraC1 VsC1c))). Qed. Lemma nl51: forall C0:dom,(r a C0)->(s C0 b)->goal. Proof. exact (fun (C0:dom)(VraC0:(r a C0))(VsC0b:(s C0 b))=>((or_ind ((nl20 C0 VraC0 VsC0b))(ex_ind (P:=fun C1:dom=>(r a C1)/\(s C1 c))(fun C1:dom=>(and_ind (nl50 C0 VraC0 VsC0b C1)))))(nl16 C0 VraC0 VsC0b))). Qed. Lemma nl52: goal. Proof. exact (((or_ind (nl12)(ex_ind (P:=fun C0:dom=>(r a C0)/\(s C0 b))(fun C0:dom=>(and_ind (nl51 C0)))))nl8)). Qed. Check nl52. End nl.