diff options
| -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) |