Mercurial > cpdt > repo
comparison src/Universes.v @ 554:93471096cdd4
Merge
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sat, 19 Aug 2017 12:14:40 -0400 |
parents | 2c8c693ddaba |
children | af97676583f3 |
comparison
equal
deleted
inserted
replaced
553:cb81f74d8c92 | 554:93471096cdd4 |
---|---|
1066 proof p | 1066 proof p |
1067 ]] | 1067 ]] |
1068 | 1068 |
1069 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *) | 1069 The first goal looks reasonable. Hypothesis [H0] is clearly contradictory, as [discriminate] can show. *) |
1070 | 1070 |
1071 discriminate. | 1071 try discriminate. (* Note: Coq 8.6 is now solving this subgoal automatically! |
1072 * This line left here to keep everything working in | |
1073 * 8.4, 8.5, and 8.6. *) | |
1072 (** %\vspace{-.15in}%[[ | 1074 (** %\vspace{-.15in}%[[ |
1073 H : proof p | 1075 H : proof p |
1074 H1 : And p q = And p0 q0 | 1076 H1 : And p q = And p0 q0 |
1075 ============================ | 1077 ============================ |
1076 proof p0 | 1078 proof p0 |