proposition: Theorem match_ex2'' : True /\ True.
proof: Proof. match goal with | [ |- _ ] => idtac "branch 1"; apply I | [ |- True /\ True ] => idtac "branch 2"; split; apply I end. Qed.
imports: Coq(Arith List) LF(IndProp) Coq(Lia)