diff options
Diffstat (limited to 'coq/ex/indent.v')
| -rw-r--r-- | coq/ex/indent.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/coq/ex/indent.v b/coq/ex/indent.v index 752bc4f9..28a56515 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -170,11 +170,14 @@ Module X. {auto. } } Qed. - - + + Lemma l2 : forall r:rec, - exists r':rec,r'.(fld1) = r.(fld2) /\ r'.(fld2) = r.(fld1). + exists r':rec,r'.(fld1) + = r.(fld2) + /\ r'.(fld2) + = r.(fld1). Proof. intros r. {{ |