diff options
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/indent.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/coq/ex/indent.v b/coq/ex/indent.v index 28a56515..a6fda706 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -174,10 +174,11 @@ Module X. Lemma l2 : forall r:rec, - exists r':rec,r'.(fld1) - = r.(fld2) - /\ r'.(fld2) - = r.(fld1). + exists r':rec, + ressai.(fld1) + = r.(fld2) + /\ r'.(fld2) + = r.(fld1). Proof. intros r. {{ |