univ_constraints_statements.v « vio « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/vio/univ_constraints_statements.v

blob: bb6b95957d051b6d3edf425896af6370d4e3e2d5 (plain)

1 2	`Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal. Proof using. intro H; rewrite H; trivial. Qed.`