We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 88d9a85 commit 6f106ffCopy full SHA for 6f106ff
1 file changed
exteq.v
@@ -64,8 +64,8 @@ Lemma extensional_and_tl :
64
extensional P -> extensional Q -> extensional (P /\_ Q).
65
Proof.
66
intros P Q eP eQ s1 s2 e. destruct e; simpl. unfold and_tl. intuition.
67
- apply eP with (Cons x s1); [constructor; assumption | assumption].
68
- apply eQ with (Cons x s1); [constructor; assumption | assumption].
+- apply eP with (Cons x s1); [constructor; assumption | assumption].
+- apply eQ with (Cons x s1); [constructor; assumption | assumption].
69
Qed.
70
71
Lemma extensional_or_tl :
0 commit comments