Section X. Let false := False. Let false_ind := False_ind. Variable dom : Set. Variable goal : Prop. Variable A0 : dom -> dom -> Prop. Variable A1 : dom -> dom -> Prop. Variable B0 : dom -> dom -> Prop. Variable B1 : dom -> dom -> Prop. Variable G : dom -> dom -> Prop. Variable S : dom -> Prop. Variable d0 : dom -> dom -> dom -> Prop. Variable d1 : dom -> dom -> dom -> Prop. Variable edge : dom -> dom -> dom -> dom -> Prop. Variable eq0 : dom -> dom -> dom -> Prop. Variable eq1 : dom -> dom -> dom -> Prop. Variable f0 : dom -> dom -> dom -> Prop. Variable f1 : dom -> dom -> dom -> Prop. Variable g0 : dom -> dom -> dom -> Prop. Variable g1 : dom -> dom -> dom -> Prop. Variable loop : dom -> dom -> dom -> Prop. Variable lt : dom -> dom -> Prop. Variable s : dom -> dom -> dom -> Prop. Variable write : dom -> Prop. Variables s0 s1 s2 a1 a2 sa1 sa2 u1 u2 b1 b2 sb1 sb2 z1 z2 v1 v2 w1 w2 x1 x2 : dom. Hypothesis domS : S s0 /\ S s1 /\ S s2. Hypothesis ltSS : lt s0 s1 /\ lt s1 s2 /\ lt s0 s2. Hypothesis dom_A0 : A0 s0 a1 /\ A0 s0 a2. Hypothesis dom_sA1 : A1 s0 sa1 /\ A1 s0 sa2. Hypothesis ext_A1 : A1 s1 u1 /\ A1 s1 u2. Hypothesis diff_s1_ai : eq0 s1 a1 a2 -> false. Hypothesis eq_s2_ai : eq0 s2 a1 a2. Hypothesis eq_s2_sau : eq1 s2 sa1 u1 /\ eq1 s2 sa2 u2 /\ eq1 s2 u1 u2. Hypothesis dom_B0 : B0 s0 b1 /\ B0 s0 b2. Hypothesis dom_sB1 : B1 s0 sb1 /\ B1 s0 sb2. Hypothesis dom_B1 : B1 s0 z1 /\ B1 s0 z2. Hypothesis ext_B1 : B1 s1 v1 /\ B1 s1 v2. Hypothesis diff_s1_bi : eq0 s1 b1 b2 -> false. Hypothesis eq_s2_bi : eq0 s2 b1 b2. Hypothesis eq_s2_sb : eq1 s2 sb1 sb2. Hypothesis eq_s2_vz : eq1 s2 v1 v2 /\ eq1 s2 v2 z2 /\ eq1 s2 z2 z1. Hypothesis diff_sbz : eq1 s2 sb1 z1 -> false. Hypothesis dom0_G : G s0 w1 /\ G s0 w2. Hypothesis ext1_G : G s1 x1 /\ G s1 x2. Hypothesis eq_s2_wx : eq1 s2 w1 w2 /\ eq1 s2 w2 x2 /\ eq1 s2 x2 x1. Hypothesis dedge : forall A B C D : dom, d1 A B C /\ d0 A B D -> edge A B C D. Hypothesis edged : forall A B C D : dom, edge A B C D -> d1 A B C /\ d0 A B D. Hypothesis loop_s : forall A B C : dom, loop A B C -> s A C B /\ edge A B C C. Hypothesis loops_sa : loop s0 sa1 a1 /\ loop s0 sa2 a2. Hypothesis loops_sb : loop s0 sb1 b1 /\ loop s0 sb2 b2. Hypothesis edges_z : edge s0 z1 b1 b1 /\ edge s0 z2 b2 b2. Hypothesis edges_u : edge s1 u1 a1 a2 /\ edge s1 u2 a2 a1. Hypothesis edges_v : edge s1 v1 b1 b2 /\ edge s1 v2 b2 b1. Hypothesis edges_w : edge s0 w1 a1 b1 /\ edge s0 w2 a2 b2. Hypothesis edges_x : edge s1 x1 a1 b2 /\ edge s1 x2 a2 b1. Hypothesis mon_A0 : forall A B C : dom, lt A B /\ A0 A C -> A0 B C. Hypothesis mon_B0 : forall A B C : dom, lt A B /\ B0 A C -> B0 B C. Hypothesis mon_A1 : forall A B C : dom, lt A B /\ A1 A C -> A1 B C. Hypothesis mon_B1 : forall A B C : dom, lt A B /\ B1 A C -> B1 B C. Hypothesis mon_G : forall A B C : dom, lt A B /\ G A C -> G B C. Hypothesis mon_eq0 : forall A B C D : dom, lt A B /\ eq0 A C D -> eq0 B C D. Hypothesis mon_eq1 : forall A B C D : dom, lt A B /\ eq1 A C D -> eq1 B C D. Hypothesis mon_d1 : forall A B C D : dom, lt A B /\ d1 A C D -> d1 B C D. Hypothesis mon_d0 : forall A B C D : dom, lt A B /\ d0 A C D -> d0 B C D. Hypothesis mon_s : forall A B C D : dom, lt A B /\ s A D C -> s B D C. Hypothesis func_d1 : forall A B C D : dom, d1 A B C /\ d1 A B D -> eq0 A C D. Hypothesis func_d0 : forall A B C D : dom, d0 A B C /\ d0 A B D -> eq0 A C D. Hypothesis func_s : forall A B C D : dom, s A B C /\ s A B D -> eq1 A C D. Hypothesis ref_eq0 : forall A B : dom, A0 A B -> eq0 A B B. Hypothesis ref_eq0 : forall A B : dom, B0 A B -> eq0 A B B. Hypothesis ref_eq1 : forall A B : dom, A1 A B -> eq1 A B B. Hypothesis ref_eq1 : forall A B : dom, B1 A B -> eq1 A B B. Hypothesis ref_eq1 : forall A B : dom, G A B -> eq1 A B B. Hypothesis sym_eq0 : forall A B C : dom, eq0 A B C -> eq0 A C B. Hypothesis sym_eq1 : forall A B C : dom, eq1 A B C -> eq1 A C B. Hypothesis trans_eq0 : forall A B C D : dom, eq0 A B C /\ eq0 A C D -> eq0 A B D. Hypothesis trans_eq1 : forall A B C D : dom, eq1 A B C /\ eq1 A C D -> eq1 A B D. Hypothesis congr_s : forall A B C D E : dom, eq0 A B C /\ eq1 A D E /\ s A B D -> s A C E. Hypothesis congr_d1 : forall A B C D E : dom, eq1 A D E /\ eq0 A B C /\ d1 A D B -> d1 A E C. Hypothesis congr_d0 : forall A B C D E : dom, eq1 A D E /\ eq0 A B C /\ d0 A D B -> d0 A E C. Hypothesis mon_f0 : forall A B C D : dom, lt A B /\ f0 A C D -> f0 B C D. Hypothesis mon_g0 : forall A B C D : dom, lt A B /\ g0 A C D -> g0 B C D. Hypothesis mon_f1 : forall A B C D : dom, lt A B /\ f1 A C D -> f1 B C D. Hypothesis mon_g1 : forall A B C D : dom, lt A B /\ g1 A C D -> g1 B C D. Hypothesis congr_f0 : forall A B C D E : dom, eq0 A B C /\ eq0 A D E /\ f0 A B D -> f0 A C E. Hypothesis congr_g0 : forall A B C D E : dom, eq0 A B C /\ eq0 A D E /\ g0 A B D -> g0 A C E. Hypothesis congr_f1 : forall A B C D E : dom, eq1 A B C /\ eq1 A D E /\ f1 A B D -> f1 A C E. Hypothesis congr_g1 : forall A B C D E : dom, eq1 A B C /\ eq1 A D E /\ g1 A B D -> g1 A C E. Hypothesis htp_fg0 : forall A B C : dom, A0 s0 A /\ A0 s0 C /\ B0 s0 B /\ f0 s0 A B /\ g0 s0 B C -> eq0 s0 A C. Hypothesis htp_gf0 : forall A B C : dom, B0 s0 A /\ B0 s0 C /\ A0 s0 B /\ g0 s0 A B /\ f0 s0 B C -> eq0 s0 A C. Hypothesis nat_f1 : forall A B C D E F G : dom, edge A F B C /\ f0 A B D /\ f0 A C E /\ f1 A F G -> edge A G D E. Hypothesis nat_f1_s : forall A B C D E : dom, f0 A B C /\ s A B D /\ s A C E -> f1 A D E. Hypothesis nat_g1 : forall A B C D E F G : dom, edge A F B C /\ g0 A B D /\ g0 A C E /\ g1 A F G -> edge A G D E. Hypothesis nat_g1_s : forall A B C D E : dom, g0 A B C /\ s A B D /\ s A C E -> g1 A D E. Hypothesis func_f0 : forall A B C D : dom, f0 A B C /\ f0 A B D -> eq0 A C D. Hypothesis func_g0 : forall A B C D : dom, g0 A B C /\ g0 A B D -> eq0 A C D. Hypothesis func_f1 : forall A B C D : dom, f1 A B C /\ f1 A B D -> eq1 A C D. Hypothesis func_g1 : forall A B C D : dom, g1 A B C /\ g1 A B D -> eq1 A C D. Hypothesis total_f0 : forall A B : dom, A0 A B -> f0 A B b1 \/ f0 A B b2. Hypothesis total_g0 : forall A B : dom, B0 A B -> g0 A B a1 \/ g0 A B a2. Hypothesis total_f1_s0 : forall A : dom, A1 s0 A -> f1 s0 A sb1 \/ f1 s0 A sb2 \/ f1 s0 A z1 \/ f1 s0 A z2. Hypothesis total_f1_s1 : forall A : dom, A1 s1 A -> f1 s1 A sb1 \/ f1 s1 A sb2 \/ f1 s1 A z1 \/ f1 s1 A z2 \/ f1 s1 A v1 \/ f1 s1 A v2. Hypothesis total_f1_s2 : forall A : dom, A1 s2 A -> f1 s2 A sb1 \/ f1 s2 A sb2 \/ f1 s2 A z1 \/ f1 s2 A z2 \/ f1 s2 A v1 \/ f1 s2 A v2. Hypothesis total_g1_s0 : forall A : dom, B1 s0 A -> g1 s0 A sa1 \/ g1 s0 A sa2. Hypothesis total_g1_s1 : forall A : dom, B1 s1 A -> g1 s1 A sa1 \/ g1 s1 A sa2 \/ g1 s1 A u1 \/ g1 s1 A u2. Hypothesis total_g1_s2 : forall A : dom, B1 s2 A -> g1 s2 A sa1 \/ g1 s2 A sa2 \/ g1 s2 A u1 \/ g1 s2 A u2. Theorem X : goal. Proof. exact (*692*)( (or_ind (fun Vf0s0a1b1 => (*498*)( (or_ind (fun Vf0s0a2b1 => (*344*)( (or_ind (fun Vg0s0b1a1 => (*334*)(false_ind goal (*333*)(diff_s1_ai (*332*)(mon_eq0 s0 s1 a1 a2 (conj (proj1 (*2*)(ltSS)(*2*)) (*331*)(sym_eq0 s0 a2 a1 (*329*)(htp_fg0 a2 b1 a1 (conj (proj2 (*3*)(dom_A0)(*3*)) (conj (proj1 (*3*)(dom_A0)(*3*)) (conj (proj1 (*8*)(dom_B0)(*8*)) (conj Vf0s0a2b1 Vg0s0b1a1)))))(*329*))(*331*)))(*332*))(*333*))(*334*)) (fun Vg0s0b1a2 => (*343*)(false_ind goal (*342*)(diff_s1_ai (*341*)(mon_eq0 s0 s1 a1 a2 (conj (proj1 (*2*)(ltSS)(*2*)) (*340*)(htp_fg0 a1 b1 a2 (conj (proj1 (*3*)(dom_A0)(*3*)) (conj (proj2 (*3*)(dom_A0)(*3*)) (conj (proj1 (*8*)(dom_B0)(*8*)) (conj Vf0s0a1b1 Vg0s0b1a2)))))(*340*)))(*341*))(*342*))(*343*))) (*323*)(total_g0 s0 b1 (proj1 (*8*)(dom_B0)(*8*)))(*323*))(*344*)) (fun Vf0s0a2b2 => (*497*)( (or_ind (fun Vg0s0b1a1 => (*487*)( (or_ind (fun Vg0s0b2a1 => (*371*)(false_ind goal (*370*)(diff_s1_ai (*369*)(mon_eq0 s0 s1 a1 a2 (conj (proj1 (*2*)(ltSS)(*2*)) (*368*)(sym_eq0 s0 a2 a1 (*366*)(htp_fg0 a2 b2 a1 (conj (proj2 (*3*)(dom_A0)(*3*)) (conj (proj1 (*3*)(dom_A0)(*3*)) (conj (proj2 (*8*)(dom_B0)(*8*)) (conj Vf0s0a2b2 Vg0s0b2a1)))))(*366*))(*368*)))(*369*))(*370*))(*371*)) (fun Vg0s0b2a2 => (*486*)( (or_ind (fun Vf1s1u1sb1 => (*380*)(false_ind goal (*379*)(diff_s1_bi (*378*)(func_d0 s1 sb1 b1 b2 (conj (*99*)(mon_d0 s0 s1 sb1 b1 (conj (proj1 (*2*)(ltSS)(*2*)) (proj2 (*25*)(edged s0 sb1 b1 b1 (proj2 (*24*)(loop_s s0 sb1 b1 (proj1 (*23*)(loops_sb)(*23*)))(*24*)))(*25*))))(*99*) (proj2 (*377*)(edged s1 sb1 b1 b2 (*376*)(nat_f1 s1 a1 a2 b1 b2 u1 sb1 (conj (proj1 (*31*)(edges_u)(*31*)) (conj (*304*)(mon_f0 s0 s1 a1 b1 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a1b1))(*304*) (conj (*345*)(mon_f0 s0 s1 a2 b2 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a2b2))(*345*) Vf1s1u1sb1))))(*376*))(*377*))))(*378*))(*379*))(*380*)) (or_ind (fun Vf1s1u1sb2 => (*386*)(false_ind goal (*385*)(diff_s1_bi (*384*)(func_d1 s1 sb2 b1 b2 (conj (proj1 (*382*)(edged s1 sb2 b1 b2 (*381*)(nat_f1 s1 a1 a2 b1 b2 u1 sb2 (conj (proj1 (*31*)(edges_u)(*31*)) (conj (*304*)(mon_f0 s0 s1 a1 b1 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a1b1))(*304*) (conj (*345*)(mon_f0 s0 s1 a2 b2 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a2b2))(*345*) Vf1s1u1sb2))))(*381*))(*382*)) (*76*)(mon_d1 s0 s1 sb2 b2 (conj (proj1 (*2*)(ltSS)(*2*)) (proj1 (*27*)(edged s0 sb2 b2 b2 (proj2 (*26*)(loop_s s0 sb2 b2 (proj2 (*23*)(loops_sb)(*23*)))(*26*)))(*27*))))(*76*)))(*384*))(*385*))(*386*)) (or_ind (fun Vf1s1u1z1 => (*407*)(false_ind goal (*406*)(diff_s1_bi (*405*)(func_d0 s1 z1 b1 b2 (conj (*103*)(mon_d0 s0 s1 z1 b1 (conj (proj1 (*2*)(ltSS)(*2*)) (proj2 (*29*)(edged s0 z1 b1 b1 (proj1 (*28*)(edges_z)(*28*)))(*29*))))(*103*) (proj2 (*404*)(edged s1 z1 b1 b2 (*403*)(nat_f1 s1 a1 a2 b1 b2 u1 z1 (conj (proj1 (*31*)(edges_u)(*31*)) (conj (*304*)(mon_f0 s0 s1 a1 b1 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a1b1))(*304*) (conj (*345*)(mon_f0 s0 s1 a2 b2 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a2b2))(*345*) Vf1s1u1z1))))(*403*))(*404*))))(*405*))(*406*))(*407*)) (or_ind (fun Vf1s1u1z2 => (*429*)(false_ind goal (*428*)(diff_s1_bi (*427*)(func_d1 s1 z2 b1 b2 (conj (proj1 (*425*)(edged s1 z2 b1 b2 (*424*)(nat_f1 s1 a1 a2 b1 b2 u1 z2 (conj (proj1 (*31*)(edges_u)(*31*)) (conj (*304*)(mon_f0 s0 s1 a1 b1 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a1b1))(*304*) (conj (*345*)(mon_f0 s0 s1 a2 b2 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a2b2))(*345*) Vf1s1u1z2))))(*424*))(*425*)) (*78*)(mon_d1 s0 s1 z2 b2 (conj (proj1 (*2*)(ltSS)(*2*)) (proj1 (*30*)(edged s0 z2 b2 b2 (proj2 (*28*)(edges_z)(*28*)))(*30*))))(*78*)))(*427*))(*428*))(*429*)) (or_ind (fun Vf1s1u1v1 => (*461*)(false_ind goal (*460*)(diff_sbz (*459*)(sym_eq1 s2 z1 sb1 (*458*)(trans_eq1 s2 z1 z2 sb1 (conj (*203*)(sym_eq1 s2 z2 z1 (proj2 (proj2 (*14*)(eq_s2_vz)(*14*))))(*203*) (*454*)(trans_eq1 s2 z2 v2 sb1 (conj (*202*)(sym_eq1 s2 v2 z2 (proj1 (proj2 (*14*)(eq_s2_vz)(*14*))))(*202*) (*447*)(sym_eq1 s2 sb1 v2 (*446*)(func_f1 s2 sa1 sb1 v2 (conj (*311*)(mon_f1 s1 s2 sa1 sb1 (conj (proj1 (proj2 (*2*)(ltSS)(*2*))) (*310*)(mon_f1 s0 s1 sa1 sb1 (conj (proj1 (*2*)(ltSS)(*2*)) (*309*)(nat_f1_s s0 a1 b1 sa1 sb1 (conj Vf0s0a1b1 (conj (proj1 (*19*)(loop_s s0 sa1 a1 (proj1 (*18*)(loops_sa)(*18*)))(*19*)) (proj1 (*24*)(loop_s s0 sb1 b1 (proj1 (*23*)(loops_sb)(*23*)))(*24*)))))(*309*)))(*310*)))(*311*) (*438*)(congr_f1 s2 u1 sa1 v1 v2 (conj (*197*)(sym_eq1 s2 sa1 u1 (proj1 (*7*)(eq_s2_sau)(*7*)))(*197*) (conj (proj1 (*14*)(eq_s2_vz)(*14*)) (*430*)(mon_f1 s1 s2 u1 v1 (conj (proj1 (proj2 (*2*)(ltSS)(*2*))) Vf1s1u1v1))(*430*))))(*438*)))(*446*))(*447*)))(*454*)))(*458*))(*459*))(*460*))(*461*)) (fun Vf1s1u1v2 => (*485*)(false_ind goal (*484*)(diff_s1_bi (*483*)(func_d1 s1 v2 b1 b2 (conj (proj1 (*479*)(edged s1 v2 b1 b2 (*478*)(nat_f1 s1 a1 a2 b1 b2 u1 v2 (conj (proj1 (*31*)(edges_u)(*31*)) (conj (*304*)(mon_f0 s0 s1 a1 b1 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a1b1))(*304*) (conj (*345*)(mon_f0 s0 s1 a2 b2 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a2b2))(*345*) Vf1s1u1v2))))(*478*))(*479*)) (proj1 (*36*)(edged s1 v2 b2 b1 (proj2 (*34*)(edges_v)(*34*)))(*36*))))(*483*))(*484*))(*485*))))))) (*375*)(total_f1_s1 u1 (proj1 (*5*)(ext_A1)(*5*)))(*375*))(*486*))) (*364*)(total_g0 s0 b2 (proj2 (*8*)(dom_B0)(*8*)))(*364*))(*487*)) (fun Vg0s0b1a2 => (*496*)(false_ind goal (*495*)(diff_s1_ai (*494*)(mon_eq0 s0 s1 a1 a2 (conj (proj1 (*2*)(ltSS)(*2*)) (*493*)(htp_fg0 a1 b1 a2 (conj (proj1 (*3*)(dom_A0)(*3*)) (conj (proj2 (*3*)(dom_A0)(*3*)) (conj (proj1 (*8*)(dom_B0)(*8*)) (conj Vf0s0a1b1 Vg0s0b1a2)))))(*493*)))(*494*))(*495*))(*496*))) (*348*)(total_g0 s0 b1 (proj1 (*8*)(dom_B0)(*8*)))(*348*))(*497*))) (*319*)(total_f0 s0 a2 (proj2 (*3*)(dom_A0)(*3*)))(*319*))(*498*)) (fun Vf0s0a1b2 => (*691*)( (or_ind (fun Vf0s0a2b1 => (*667*)( (or_ind (fun Vg0s0b1a1 => (*529*)(false_ind goal (*528*)(diff_s1_ai (*527*)(mon_eq0 s0 s1 a1 a2 (conj (proj1 (*2*)(ltSS)(*2*)) (*526*)(sym_eq0 s0 a2 a1 (*524*)(htp_fg0 a2 b1 a1 (conj (proj2 (*3*)(dom_A0)(*3*)) (conj (proj1 (*3*)(dom_A0)(*3*)) (conj (proj1 (*8*)(dom_B0)(*8*)) (conj Vf0s0a2b1 Vg0s0b1a1)))))(*524*))(*526*)))(*527*))(*528*))(*529*)) (fun Vg0s0b1a2 => (*666*)( (or_ind (fun Vg0s0b2a1 => (*660*)( (or_ind (fun Vf1s1u1sb1 => (*554*)(false_ind goal (*553*)(diff_s1_bi (*552*)(func_d1 s1 sb1 b1 b2 (conj (*75*)(mon_d1 s0 s1 sb1 b1 (conj (proj1 (*2*)(ltSS)(*2*)) (proj1 (*25*)(edged s0 sb1 b1 b1 (proj2 (*24*)(loop_s s0 sb1 b1 (proj1 (*23*)(loops_sb)(*23*)))(*24*)))(*25*))))(*75*) (proj1 (*551*)(edged s1 sb1 b2 b1 (*550*)(nat_f1 s1 a1 a2 b2 b1 u1 sb1 (conj (proj1 (*31*)(edges_u)(*31*)) (conj (*499*)(mon_f0 s0 s1 a1 b2 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a1b2))(*499*) (conj (*515*)(mon_f0 s0 s1 a2 b1 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a2b1))(*515*) Vf1s1u1sb1))))(*550*))(*551*))))(*552*))(*553*))(*554*)) (or_ind (fun Vf1s1u1sb2 => (*560*)(false_ind goal (*559*)(diff_s1_bi (*558*)(func_d0 s1 sb2 b1 b2 (conj (proj2 (*556*)(edged s1 sb2 b2 b1 (*555*)(nat_f1 s1 a1 a2 b2 b1 u1 sb2 (conj (proj1 (*31*)(edges_u)(*31*)) (conj (*499*)(mon_f0 s0 s1 a1 b2 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a1b2))(*499*) (conj (*515*)(mon_f0 s0 s1 a2 b1 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a2b1))(*515*) Vf1s1u1sb2))))(*555*))(*556*)) (*101*)(mon_d0 s0 s1 sb2 b2 (conj (proj1 (*2*)(ltSS)(*2*)) (proj2 (*27*)(edged s0 sb2 b2 b2 (proj2 (*26*)(loop_s s0 sb2 b2 (proj2 (*23*)(loops_sb)(*23*)))(*26*)))(*27*))))(*101*)))(*558*))(*559*))(*560*)) (or_ind (fun Vf1s1u1z1 => (*581*)(false_ind goal (*580*)(diff_s1_bi (*579*)(func_d1 s1 z1 b1 b2 (conj (*77*)(mon_d1 s0 s1 z1 b1 (conj (proj1 (*2*)(ltSS)(*2*)) (proj1 (*29*)(edged s0 z1 b1 b1 (proj1 (*28*)(edges_z)(*28*)))(*29*))))(*77*) (proj1 (*578*)(edged s1 z1 b2 b1 (*577*)(nat_f1 s1 a1 a2 b2 b1 u1 z1 (conj (proj1 (*31*)(edges_u)(*31*)) (conj (*499*)(mon_f0 s0 s1 a1 b2 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a1b2))(*499*) (conj (*515*)(mon_f0 s0 s1 a2 b1 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a2b1))(*515*) Vf1s1u1z1))))(*577*))(*578*))))(*579*))(*580*))(*581*)) (or_ind (fun Vf1s1u1z2 => (*603*)(false_ind goal (*602*)(diff_s1_bi (*601*)(func_d0 s1 z2 b1 b2 (conj (proj2 (*599*)(edged s1 z2 b2 b1 (*598*)(nat_f1 s1 a1 a2 b2 b1 u1 z2 (conj (proj1 (*31*)(edges_u)(*31*)) (conj (*499*)(mon_f0 s0 s1 a1 b2 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a1b2))(*499*) (conj (*515*)(mon_f0 s0 s1 a2 b1 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a2b1))(*515*) Vf1s1u1z2))))(*598*))(*599*)) (*105*)(mon_d0 s0 s1 z2 b2 (conj (proj1 (*2*)(ltSS)(*2*)) (proj2 (*30*)(edged s0 z2 b2 b2 (proj2 (*28*)(edges_z)(*28*)))(*30*))))(*105*)))(*601*))(*602*))(*603*)) (or_ind (fun Vf1s1u1v1 => (*626*)(false_ind goal (*625*)(diff_s1_bi (*624*)(func_d1 s1 v1 b1 b2 (conj (proj1 (*35*)(edged s1 v1 b1 b2 (proj1 (*34*)(edges_v)(*34*)))(*35*)) (proj1 (*621*)(edged s1 v1 b2 b1 (*620*)(nat_f1 s1 a1 a2 b2 b1 u1 v1 (conj (proj1 (*31*)(edges_u)(*31*)) (conj (*499*)(mon_f0 s0 s1 a1 b2 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a1b2))(*499*) (conj (*515*)(mon_f0 s0 s1 a2 b1 (conj (proj1 (*2*)(ltSS)(*2*)) Vf0s0a2b1))(*515*) Vf1s1u1v1))))(*620*))(*621*))))(*624*))(*625*))(*626*)) (fun Vf1s1u1v2 => (*659*)(false_ind goal (*658*)(diff_sbz (*657*)(trans_eq1 s2 sb1 sb2 z1 (conj (*13*)(eq_s2_sb)(*13*) (*656*)(sym_eq1 s2 z1 sb2 (*655*)(trans_eq1 s2 z1 z2 sb2 (conj (*203*)(sym_eq1 s2 z2 z1 (proj2 (proj2 (*14*)(eq_s2_vz)(*14*))))(*203*) (*651*)(trans_eq1 s2 z2 v2 sb2 (conj (*202*)(sym_eq1 s2 v2 z2 (proj1 (proj2 (*14*)(eq_s2_vz)(*14*))))(*202*) (*644*)(sym_eq1 s2 sb2 v2 (*643*)(func_f1 s2 sa1 sb2 v2 (conj (*506*)(mon_f1 s1 s2 sa1 sb2 (conj (proj1 (proj2 (*2*)(ltSS)(*2*))) (*505*)(mon_f1 s0 s1 sa1 sb2 (conj (proj1 (*2*)(ltSS)(*2*)) (*504*)(nat_f1_s s0 a1 b2 sa1 sb2 (conj Vf0s0a1b2 (conj (proj1 (*19*)(loop_s s0 sa1 a1 (proj1 (*18*)(loops_sa)(*18*)))(*19*)) (proj1 (*26*)(loop_s s0 sb2 b2 (proj2 (*23*)(loops_sb)(*23*)))(*26*)))))(*504*)))(*505*)))(*506*) (*635*)(congr_f1 s2 u1 sa1 v1 v2 (conj (*197*)(sym_eq1 s2 sa1 u1 (proj1 (*7*)(eq_s2_sau)(*7*)))(*197*) (conj (proj1 (*14*)(eq_s2_vz)(*14*)) (*634*)(congr_f1 s2 u1 u1 v2 v1 (conj (*172*)(mon_eq1 s1 s2 u1 u1 (conj (proj1 (proj2 (*2*)(ltSS)(*2*))) (*171*)(ref_eq1 s1 u1 (proj1 (*5*)(ext_A1)(*5*)))(*171*)))(*172*) (conj (*201*)(sym_eq1 s2 v1 v2 (proj1 (*14*)(eq_s2_vz)(*14*)))(*201*) (*627*)(mon_f1 s1 s2 u1 v2 (conj (proj1 (proj2 (*2*)(ltSS)(*2*))) Vf1s1u1v2))(*627*))))(*634*))))(*635*)))(*643*))(*644*)))(*651*)))(*655*))(*656*)))(*657*))(*658*))(*659*))))))) (*549*)(total_f1_s1 u1 (proj1 (*5*)(ext_A1)(*5*)))(*549*))(*660*)) (fun Vg0s0b2a2 => (*665*)(false_ind goal (*664*)(diff_s1_ai (*663*)(mon_eq0 s0 s1 a1 a2 (conj (proj1 (*2*)(ltSS)(*2*)) (*662*)(htp_fg0 a1 b2 a2 (conj (proj1 (*3*)(dom_A0)(*3*)) (conj (proj2 (*3*)(dom_A0)(*3*)) (conj (proj2 (*8*)(dom_B0)(*8*)) (conj Vf0s0a1b2 Vg0s0b2a2)))))(*662*)))(*663*))(*664*))(*665*))) (*545*)(total_g0 s0 b2 (proj2 (*8*)(dom_B0)(*8*)))(*545*))(*666*))) (*518*)(total_g0 s0 b1 (proj1 (*8*)(dom_B0)(*8*)))(*518*))(*667*)) (fun Vf0s0a2b2 => (*690*)( (or_ind (fun Vg0s0b1a1 => (*680*)(false_ind goal (*679*)(diff_s1_bi (*678*)(mon_eq0 s0 s1 b1 b2 (conj (proj1 (*2*)(ltSS)(*2*)) (*677*)(htp_gf0 b1 a1 b2 (conj (proj1 (*8*)(dom_B0)(*8*)) (conj (proj2 (*8*)(dom_B0)(*8*)) (conj (proj1 (*3*)(dom_A0)(*3*)) (conj Vg0s0b1a1 Vf0s0a1b2)))))(*677*)))(*678*))(*679*))(*680*)) (fun Vg0s0b1a2 => (*689*)(false_ind goal (*688*)(diff_s1_bi (*687*)(mon_eq0 s0 s1 b1 b2 (conj (proj1 (*2*)(ltSS)(*2*)) (*686*)(htp_gf0 b1 a2 b2 (conj (proj1 (*8*)(dom_B0)(*8*)) (conj (proj2 (*8*)(dom_B0)(*8*)) (conj (proj2 (*3*)(dom_A0)(*3*)) (conj Vg0s0b1a2 Vf0s0a2b2)))))(*686*)))(*687*))(*688*))(*689*))) (*671*)(total_g0 s0 b1 (proj1 (*8*)(dom_B0)(*8*)))(*671*))(*690*))) (*514*)(total_f0 s0 a2 (proj2 (*3*)(dom_A0)(*3*)))(*514*))(*691*))) (*303*)(total_f0 s0 a1 (proj1 (*3*)(dom_A0)(*3*)))(*303*))(*692*). Qed. End X.