include "delayed_updating/substitution/fsubst.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 * *