Section dpe. 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 re:dom->dom->Prop. Variable a b c:dom. Hypothesis assump:(re a b)/\(re a c). Hypothesis goal_ax:forall A:dom,(re b A)/\(re c A)->goal. Hypothesis ref_e:forall A:dom,(e A A). Hypothesis sym_e:forall A B:dom,(e A B)->(e B A). Hypothesis congl:forall A B C:dom,(e A B)/\(re B C)->(re A C). Hypothesis e_in_re:forall A B:dom,(e A B)->(re A B). Hypothesis r_in_re:forall A B:dom,(r A B)->(re A B). Hypothesis e_or_r:forall A B:dom,(re A B)->(e A B) \/ (r A B). Hypothesis dp_r:forall A B C:dom,(r A B)/\(r A C)->(exists D:dom,(r B D)/\(r C D)). Lemma dpe1: (re a b)/\(re a c). Proof. exact (assump). Qed. Lemma dpe3: (e b b). Proof. exact ((ref_e b)). Qed. Lemma dpe4: (e c c). Proof. exact ((ref_e c)). Qed. Lemma dpe6: (re b b). Proof. exact (((e_in_re b b) dpe3)). Qed. Lemma dpe7: (re c c). Proof. exact (((e_in_re c c) dpe4)). Qed. Lemma dpe8: (e a b) \/ (r a b). Proof. exact (((e_or_r a b) (proj1 dpe1))). Qed. Lemma dpe9: (e a b)->(e b a). Proof. exact (fun (Veab:(e a b))=>((sym_e a b) Veab)). Qed. Lemma dpe10: (e a b)->(re b c). Proof. exact (fun (Veab:(e a b))=>((congl b a c) (conj (dpe9 Veab) (proj2 dpe1)))). Qed. Lemma dpe11: (e a b)->goal. Proof. exact (fun (Veab:(e a b))=>((goal_ax c) (conj (dpe10 Veab) dpe7))). Qed. Lemma dpe12: (r a b)->(e a c) \/ (r a c). Proof. exact (fun (Vrab:(r a b))=>((e_or_r a c) (proj2 dpe1))). Qed. Lemma dpe13: (r a b)->(e a c)->(e c a). Proof. exact (fun (Vrab:(r a b))(Veac:(e a c))=>((sym_e a c) Veac)). Qed. Lemma dpe14: (r a b)->(e a c)->(re c b). Proof. exact (fun (Vrab:(r a b))(Veac:(e a c))=>((congl c a b) (conj (dpe13 Vrab Veac) (proj1 dpe1)))). Qed. Lemma dpe15: (r a b)->(e a c)->goal. Proof. exact (fun (Vrab:(r a b))(Veac:(e a c))=>((goal_ax b) (conj dpe6 (dpe14 Vrab Veac)))). Qed. Lemma dpe16: (r a b)->(r a c)->(exists A:dom,(r b A)/\(r b A)). Proof. exact (fun (Vrab:(r a b))(Vrac:(r a c))=>((dp_r a b b) (conj Vrab Vrab))). Qed. Lemma dpe20: (r a b)->(r a c)->forall C0:dom,(r b C0)->(r b C0)->(exists A:dom,(r b A)/\(r c A)). Proof. exact (fun (Vrab:(r a b))(Vrac:(r a c))(C0:dom)(VrbC0:(r b C0))(VrbC0:(r b C0))=>((dp_r a b c) (conj Vrab Vrac))). Qed. Lemma dpe23: (r a b)->(r a c)->forall C0:dom,(r b C0)->(r b C0)->forall C1:dom,(r b C1)->(r c C1)->(re b C1). Proof. exact (fun (Vrab:(r a b))(Vrac:(r a c))(C0:dom)(VrbC0:(r b C0))(VrbC0:(r b C0))(C1:dom)(VrbC1:(r b C1))(VrcC1:(r c C1))=>((r_in_re b C1) VrbC1)). Qed. Lemma dpe24: (r a b)->(r a c)->forall C0:dom,(r b C0)->(r b C0)->forall C1:dom,(r b C1)->(r c C1)->(re c C1). Proof. exact (fun (Vrab:(r a b))(Vrac:(r a c))(C0:dom)(VrbC0:(r b C0))(VrbC0:(r b C0))(C1:dom)(VrbC1:(r b C1))(VrcC1:(r c C1))=>((r_in_re c C1) VrcC1)). Qed. Lemma dpe25: (r a b)->(r a c)->forall C0:dom,(r b C0)->(r b C0)->forall C1:dom,(r b C1)->(r c C1)->goal. Proof. exact (fun (Vrab:(r a b))(Vrac:(r a c))(C0:dom)(VrbC0:(r b C0))(VrbC0:(r b C0))(C1:dom)(VrbC1:(r b C1))(VrcC1:(r c C1))=>((goal_ax C1) (conj (dpe23 Vrab Vrac C0 VrbC0 VrbC0 C1 VrbC1 VrcC1) (dpe24 Vrab Vrac C0 VrbC0 VrbC0 C1 VrbC1 VrcC1)))). Qed. Lemma dpe26: (r a b)->(r a c)->forall C0:dom,(r b C0)->(r b C0)->goal. Proof. exact (fun (Vrab:(r a b))(Vrac:(r a c))(C0:dom)(VrbC0:(r b C0))(VrbC0:(r b C0))=>((ex_ind (P:=fun C1:dom=>(r b C1)/\(r c C1))(fun C1:dom=>(and_ind (dpe25 Vrab Vrac C0 VrbC0 VrbC0 C1))))(dpe20 Vrab Vrac C0 VrbC0 VrbC0))). Qed. Lemma dpe27: (r a b)->(r a c)->goal. Proof. exact (fun (Vrab:(r a b))(Vrac:(r a c))=>((ex_ind (P:=fun C0:dom=>(r b C0)/\(r b C0))(fun C0:dom=>(and_ind (dpe26 Vrab Vrac C0))))(dpe16 Vrab Vrac))). Qed. Lemma dpe28: (r a b)->goal. Proof. exact (fun (Vrab:(r a b))=>((or_ind ((dpe15 Vrab))((dpe27 Vrab)))(dpe12 Vrab))). Qed. Lemma dpe29: goal. Proof. exact (((or_ind (dpe11)(dpe28))dpe8)). Qed. Check dpe29. End dpe.