proposition: Lemma unlift_example3 : forall (P Q R : Type), [ P ] -> [ P -> Q ] -> [ Q -> R ] -> R.
proof: Proof. intros P Q R p pq qr. Abort. Lemma stronger_inhabited_in_hypothese : forall A B, ([A] -> [B]) -> (A -> [B]). Proof. eauto. Qed.
imports: Monad InhabitedTactics