(**************************************************************************)
include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/syntax/prototerm_equivalence.ma".
+include "delayed_updating/syntax/prototerm_eq.ma".
+
+(* FOCALIZED SUBSTITUTION ***************************************************)
(* Constructions with subset_equivalence ************************************)
+lemma fsubst_empty_rc (t) (u):
+ u ā t[āšāu].
+#t #u @conj #p
+[ #Hp /3 width=3 by or_introl, ex2_intro/ ]
+* *
+[ #r #Hr #H0 destruct // ]
+#H1p #H2p elim H2p -H2p //
+qed.
+
lemma subset_inclusion_fsubst_bi (t1) (t2) (u1) (u2) (p):
t1 ā t2 ā u1 ā u2 ā t1[āpāu1] ā t2[āpāu2].
#t1 #t2 #u1 #u2 #p #Ht #Hu #q * *
]
qed.
-lemma fsubst_eq_repl (t1) (t2) (u1) (u2) (p):
- t1 ā t2 ā u1 ā u2 ā t1[āpāu1] ā t2[āpāu2].
-#t1 #t2 #u1 #u2 #p * #H1t #H2t * #H1u #H2u
+lemma fsubst_eq_repl (t1) (t2) (u1) (u2) (p1) (p2):
+ t1 ā t2 ā p1 = p2 ā u1 ā u2 ā t1[āp1āu1] ā t2[āp2āu2].
+#t1 #t2 #u1 #u2 #p1 #p2 * #H1t #H2t #Hp * #H1u #H2u
/3 width=5 by conj, subset_inclusion_fsubst_bi/
qed.