proposition: Lemma exists_Sn (P : nat -> Prop) : (exists n, P (S n)) -> exists n, P n.
proof: Proof. intros [n H]. eexists; eauto. Qed.
imports: String List RoseTrees Show State Producer Generators Enumerators Classes DependentClasses Checker Decidability TacticsUtil Ltac2(Ltac2)