proposition: Lemma test6 : forall (x y z : Prop), x = y -> y = z -> x = z.
proof: Proof. MProof. intros x y z H G. ltac transitivity [m:Dyn y]. ltac "Coq.Init.Ltac.revgoals" [m:]. exact H. exact G. Qed.
imports: Bool.Bool Mtac2.Mtac2 Lia