proposition: Lemma subeq_inversion : forall u θ θ', sub θ u = sub θ' u -> forall x, In x (vars u) -> θ x = θ' x.
proof: Proof. intros u; pattern u; apply term_ind with (Q := fun nu (us : terms nu) => forall θ θ', Vmap (sub θ) us = Vmap (sub θ') us -> forall x, In x (vars_vec us) -> θ x = θ' x). intros x θ θ'; simpl; intros Hθθ' y H. by case H; [intros Hxy; subst x|idtac]; tauto. intros f ts IHs θ θ'. simpl sub. intros Hθθ' y. rewrite vars_fun; intros Hvars; apply IHs; try done. by rewrite (fun_eq Hθθ'). by intros θ θ' _ x; simpl; tauto. intros t nt ts IH IHs θ θ'; simpl; intros H; Veqtac. intros x Hx; case (in_app_or Hx); clear Hx; intros Hx. by apply IH. by apply IHs. Qed.
imports: CoLoR(AInterpretation AContext VecUtil NatUtil LogicUtil ListUtil EqUtil)