proposition: Lemma sub_eq_is_sol : forall s1 t1 s2 t2, (forall x, In x (vars t1) -> In x (vars t2) -> False) -> sub s1 t1 = sub s2 t2 -> unifiable t1 t2.
proof: Proof. intros. set (s := fun x => match In_dec x (vars t1) with | left _ => s1 x | right _ => s2 x end). exists s. unfold is_sol, mk_problem. simpl. split_all. unfold is_sol_eqn. simpl. trans (sub s1 t1). apply sub_eq. intros. unfold s. case (In_dec x (vars t1)). refl. contr. rewrite H0. apply sub_eq. intros. unfold s. case (In_dec x (vars t1)). intro. exfalso. exact (H x i H1). refl. Qed.
imports: Coq(Relations Wellfounded) CoLoR(ASubstitution ATerm EqUtil ListUtil LogicUtil VecUtil AVariables BoolUtil NatUtil SN AVariables Lexico)