proposition: Lemma nmatches_extend_compatP : forall nu (us : terms nu) nt (ts : terms nt) m m', Vfold2 m matches_r us ts = Some m' -> forall θ, Vmap (sub (m ⊕ θ)) us =V ts -> forall x, (m ⊕ θ) x = (m' ⊕ θ) x.
proof: Proof. induction us as [|u nu us IH]; destruct ts as [|t nt ts]; intros m₁ m₂; try discr. by simpl; intros H; inversion_clear H. simpl; case_eq (Vfold2 m₁ matches_r us ts); try discr. intros m H₁ H₂ θ H x; elim (proj1 (andb_true_iff _ _) H). intros Hu Hus; trans ((m ⊕ θ) x). by apply (IH _ _ _ _ H₁). apply (matches_extend_compatP H₂). rewrite <- (proj1 (beq_term_ok _ _) Hu). by apply sub_eq; intros y _; sym; apply (IH _ _ _ _ H₁). Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)