proposition: Theorem substi_exists : forall s x t, { t' | substi s x t t'}.
proof: Proof. intros s x0 t; induction t; intros; eauto. - destruct (dec_eq x0 s0); subst; eauto. - destruct IHt1, IHt2; eauto. - destruct (dec_eq x0 s0), IHt; subst; eauto. - destruct IHt1, IHt2, IHt3; eauto. Qed.
imports: QuickChick(QuickChick) Coq(Nat) Coq(Arith.Arith) Coq(Logic.FunctionalExtensionality)