-theorem rex_conf: ∀R1,R2.
- rex_fsge_compatible R1 →
- rex_fsge_compatible R2 →
- R_confluent2_rex R1 R2 R1 R2 →
- ∀T. confluent2 … (rex R1 T) (rex R2 T).
+theorem rex_conf1 (R1) (R2):
+ rex_fsge_compatible R2 → (c_reflexive … R2) →
+ R_replace3_rex R1 R2 R1 R2 →
+ ∀T. confluent1 … (rex R1 T) (rex R2 T).
+#R1 #R2 #H1R #H2R #H3R #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL12
+lapply (frees_mono … Hf1 … Hf2) -Hf1 #Hf12
+lapply (sex_eq_repl_back … HL1 … Hf12) -f1 #HL1
+elim (frees_sex_conf_fsge … Hf2 … HL12) // #g2 #Hg2 #Hfg2
+lapply (sex_repl … HL1 … HL12 L ?) //
+[ /3 width=1 by sex_refl, ext2_refl/
+| -g2 #g2 * #I1 [| #V1 ] #K1 #n #HLK1 #Hgf2 #Z1 #H1 #Z2 #H2 #Y1 #HY1 #Y2 #HY2 #Z #HZ
+ [ lapply (ext2_inv_unit_sn … H1) -H1 #H destruct
+ lapply (ext2_inv_unit_sn … H2) -H2 #H destruct
+ lapply (ext2_inv_unit_sn … HZ) -HZ #H destruct
+ /2 width=1 by ext2_unit/
+ | elim (ext2_inv_pair_sn … H1) -H1 #W1 #HW1 #H destruct
+ elim (ext2_inv_pair_sn … H2) -H2 #W2 #HW2 #H destruct
+ elim (ext2_inv_pair_sn … HZ) -HZ #W #HW #H destruct
+ elim (frees_inv_drops_next … Hf2 … HLK1 … Hgf2) -Hf2 -HLK1 -Hgf2 #g0 #Hg0 #Hg02
+ lapply (sle_sex_trans … HY1 … Hg02) // -HY1 #HY1
+ lapply (sle_sex_trans … HY2 … Hg02) // -HY2 #HY2
+ /4 width=9 by ext2_pair, ex2_intro/
+ ]
+| /3 width=5 by sle_sex_trans, ex2_intro/
+]
+qed-.
+
+theorem rex_conf (R1) (R2):
+ rex_fsge_compatible R1 → rex_fsge_compatible R2 →
+ R_confluent2_rex R1 R2 R1 R2 →
+ ∀T. confluent2 … (rex R1 T) (rex R2 T).