proposition: Theorem substi_uniq : forall s x t t' t'', substi s x t t' -> substi s x t t'' -> t' = t''.
proof: Proof. intros s x t. induction t; intros; inversion H0; inversion H; subst; eauto; try (exfalso; eauto; fail). - f_equal. + apply IHt1; auto. + apply IHt2; auto. - f_equal; apply IHt; auto. - f_equal. + apply IHt1; auto. + apply IHt2; auto. + apply IHt3; auto. Qed.
imports: QuickChick(QuickChick) Coq(Nat) Coq(Arith.Arith) Coq(Logic.FunctionalExtensionality)