proposition: Lemma matches_r_complete : \matches_complete /\ \nmatches_complete.
proof: Proof. apply term_ind_comb. intros x t m H; elim H; simpl; unfold compose. case_eq (VM.find x m); [intros mx Hfind _ Ht | intros Hfind _ _]; unfold exmatch; rewrite Hfind; try done. by rewrite (proj2 (beq_term_ok _ _) (sym_eq Ht)); discr. intros g us IH t m H; destruct t as [x|f nt]; elim H; intros θ Hθ; rewrite sub_fun in Hθ; try discr. inversion_clear Hθ; simpl; rewrite (beq_refl (@beq_symb_ok Sig)). apply IH; exists θ; rewrite beq_vec_refl; try done. by apply beq_term_ok. destruct ts as [|t nt ts]; intros m H; simpl. by discr. by elim H; intros θ Hθ; simpl in Hθ. intros u nu us IH IHs; destruct ts as [|t nt ts]; intros m H. by elim H; intros θ Hθ; simpl in Hθ. elim H; intros θ Hθ; simpl in Hθ. case (proj1 (andb_true_iff _ _) Hθ); intros Hu Hus. simpl; case_eq (Vfold2 m matches_r us ts). intros m' Hm'; apply IH; exists θ. rewrite <- (proj1 (beq_term_ok _ _) Hu). apply sub_eq; intros x _; sym. by apply nmatches_extend_compatP with _ us _ ts. intros Hfold _; eapply IHs; [idtac | ehyp]. by exists θ. Qed.
imports: Coq(Peano_dec Bool) CoLoR(LogicUtil EqUtil NatUtil VecUtil ATerm ASubstitution FSetUtil FMapUtil ListUtil)