forked from GitHub/gf-core
*** empty log message ***
This commit is contained in:
@@ -27,7 +27,7 @@ fun
|
||||
|
||||
Univ : (A : Dom) -> (Elem A -> Prop) -> Prop ;
|
||||
Exist : (A : Dom) -> (Elem A -> Prop) -> Prop ;
|
||||
|
||||
|
||||
-- progressive implication ŕ la type theory
|
||||
ImplP : (A : Prop) -> (Proof A -> Prop) -> Prop ;
|
||||
|
||||
|
||||
Reference in New Issue
Block a user