proposition: Lemma matches_extend_compatP : forall u t m m', matches_r u t m = Some m' -> forall θ, u ! (m ⊕ θ) = t -> forall x, (m ⊕ θ) x = (m' ⊕ θ) x.
proof: Proof. intros u t m m' H θ Hθ x; unfold compose. case_eq (VM.find x m); case_eq (VM.find x m'). intros v₂ Hv₂ v₁ Hv₁; rewrite <- (matches_monP H) in Hv₂. congruence. by rewrite VMF.mem_find_b, Hv₁. intros Hm' v Hv; rewrite <- (matches_monP H) in Hm'. congruence. by rewrite VMF.mem_find_b, Hv. intros v Hv Hm; rewrite <- (composeI θ Hm). rewrite <- (subst_of_matchingE Hv). apply subeq_inversion with u. by rewrite (proj1 matches_r_correct _ _ _ _ H). apply (proj2 (AVariables.in_vars_mem _ _)). apply (matches_var_minadded H); rewrite VMF.mem_find_b. by rewrite Hm. by rewrite Hv. refl. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)