proposition: Lemma nmatches_submon : forall nu (us : terms nu) nt (ts : terms nt) θ, (Vmap (sub \S(θ)) us) =V ts -> (forall x, VS.mem x (vars_vec us) -> VM.mem x θ) -> forall u t θ', matches_r u t θ = Some θ' -> (Vmap (sub \S(θ')) us) =V ts.
proof: Proof. induction us as [|u nu us IH]; destruct ts as [|t nt ts]; try discr. intros; refl. intros θ Heq Hmem u' t' θ' Hθθ'; simpl in Heq |- *. elim (proj1 (andb_true_iff _ _) Heq); intros Htu Hts_uts. unfold is_true; apply (proj2 (andb_true_iff _ _)); split. apply (proj2 (beq_term_ok _ _)); apply matches_submon with θ u' t'. by apply (proj1 (beq_term_ok _ _)). by intros x Hx; apply Hmem; simpl; rewrite VSF.union_b, Hx, orb_true_l. hyp. apply IH with θ u' t'; try hyp. by intros x Hx; apply Hmem; simpl; rewrite VSF.union_b, Hx, orb_true_r. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)