Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Simplify proof.

  • Loading branch information...
commit 9069a093973ac6893c03a33f4c59bab884391cef 1 parent 320ff97
@pi8027 pi8027 authored
Showing with 1 addition and 3 deletions.
  1. +1 −3 2012-04-19/ConstructiveLogic.v
View
4 2012-04-19/ConstructiveLogic.v
@@ -1,4 +1,3 @@
-
Require Import Arith.
Require Import List.
@@ -16,8 +15,7 @@ Inductive hilbert : assump -> proposition -> Prop :=
| Hasp : forall {a : assump} {p : proposition}, In p a -> hilbert a p
| Hstarling : forall {a : assump} {p1 p2 p3 : proposition},
hilbert a ((p1 *-> p2 *-> p3) *-> (p1 *-> p2) *-> p1 *-> p3)
- | Hkestrel : forall {a : assump} {p1 p2 : proposition},
- hilbert a (p1 *-> p2 *-> p1).
+ | Hkestrel : forall {a : assump} {p1 p2 : proposition}, hilbert a (p1 *-> p2 *-> p1).
Inductive nd : assump -> proposition -> Prop :=
NDmp : forall {a : assump} {p1 p2 : proposition}, nd a (p1 *-> p2) -> nd a p1 -> nd a p2
Please sign in to comment.
Something went wrong with that request. Please try again.