proposition: Lemma matches_some_ind : \matchesP /\ \matchesPs.
proof: Proof. apply term_ind_comb. hyp. intros g us Hus t θ θ' Hθθ'; destruct t as [y|f ts]; try discr. simpl in Hθθ'; case_eq (f =S g); intros Hfg; rewrite Hfg in Hθθ'; try discr. by apply Hfun; auto; rewrite (proj1 beq_symb_ok Hfg). intros nt ts θ θ'; destruct ts as [|t nt ts]; try discr. by inversion_clear 1; apply Hnil. intros u nu us Hu Hus nt ts θ θ'. destruct ts as [|t nt ts]; try discr; simpl Vfold2. case_eq (Vfold2 θ matches_r us ts); try discr; intros Ω HθΩ HΩθ'. by apply Hcns with Ω; auto. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)