diff options
Diffstat (limited to 'mathcomp/ssrtest/ipatalternation.v')
| -rw-r--r-- | mathcomp/ssrtest/ipatalternation.v | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/mathcomp/ssrtest/ipatalternation.v b/mathcomp/ssrtest/ipatalternation.v deleted file mode 100644 index 65f3760..0000000 --- a/mathcomp/ssrtest/ipatalternation.v +++ /dev/null @@ -1,8 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - - -Lemma test1 : Prop -> Prop -> Prop -> Prop -> Prop -> True = False -> Prop -> True \/ True. -by move=> A /= /= /= B C {A} {B} ? _ {C} {1}-> *; right. -Qed.
\ No newline at end of file |