proposition: Theorem match_ex5 : forall (P Q R : Prop), P -> Q -> R.
proof: Proof. intros P Q R HP HQ. Fail match goal with | [ H : _ |- _ ] => idtac H; apply H end. Abort. Theorem match_ex5 : forall (P Q : Prop), P -> Q -> P. Proof. intros P Q HP HQ. match goal with | [ H : ?X |- ?X ] => idtac H; apply H end. Qed.
imports: Coq(Arith List) LF(IndProp) Coq(Lia)