diff options
| author | Théo Zimmermann | 2019-10-30 17:10:05 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-10-30 17:19:57 +0100 |
| commit | fa822f0762df1c46d8e179afb9b408a927fff149 (patch) | |
| tree | 145cfc25bff38d747437750ce31f2de288a77dde | |
| parent | 5d1f7461f74f727d0394e904c3ee820134b22c64 (diff) | |
Use bullets and indentation (but the result rendering is weird).
| -rw-r--r-- | doc/sphinx/language/cic.rst | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 9e4210793e..6410620b40 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1074,10 +1074,13 @@ between universes for inductive types in the Type hierarchy. Lemma contradiction : False. Proof. - enough (I /\ ~ I) as [] by contradiction. - split. - apply not_I_I; intro; now apply I_not_I. - intro; now apply I_not_I. + enough (I /\ ~ I) as [] by contradiction. + split. + - apply not_I_I. + intro. + now apply I_not_I. + - intro. + now apply I_not_I. Qed. .. example:: Negative occurrence (second example) |