proposition: Theorem intuition_simplify1 : forall (P : Prop), ~~P -> P.
proof: Proof. intuition. Abort. Theorem intuition_simplify2 : forall (x y : nat) (P Q : nat -> Prop), x = y /\ (P x -> Q x) /\ P x -> Q y. Proof. Fail congruence. intuition. congruence. Qed.
imports: Coq(Arith List) LF(IndProp) Coq(Lia)