proposition: Lemma restrict_domain_subs_aeq : forall u v, (forall s, (forall x, ~In x (union (fv u) (fv v)) -> s x = Var x) -> subs s u ~~ subs s v) -> forall s, subs s u ~~ subs s v.
proof: Proof. intros u v h s. set (s' := restrict (union (fv u) (fv v)) s). rewrite subs_seq with (s':=s'). rewrite subs_seq with (s:=s) (s':=s'). apply h. intros x h'. unfold s', Def.restrict; ens. rewrite not_mem_iff in h'. rewrite h'. refl. unfold s'. apply seq_restrict. apply union_subset_2. unfold s'. apply seq_restrict. apply union_subset_1. Qed.
imports: Coq(Wf_nat Morphisms Basics Equivalence) CoLoR(BoolUtil RelUtil LogicUtil SN VecUtil NatUtil VecOrd)