diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Init/Logic.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 375495c88..50f853f0e 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -370,7 +370,7 @@ Module EqNotations. End EqNotations. Import EqNotations. -Set Printing Universes. + Lemma rew_opp_r : forall A (P:A->Type) (x y:A) (H:x=y) (a:P y), rew H in rew <- H in a = a. Proof. intros. |