proposition: Lemma exfalso_none_some_false (P : Prop) : (fun (_ : unit) => None) tt = Some false -> P.
proof: Proof. congruence. Qed.
imports: String List RoseTrees Show State Producer Generators Enumerators Classes DependentClasses Checker Decidability TacticsUtil Ltac2(Ltac2)