SHOW:
|
|
- or go back to the newest paste.
| 1 | - | KB: |
| 1 | + | |
| 2 | ?A ( True ) -> ?A | |
| 3 | R ?A ?B -> ( ?A AND ?B ) : Set | |
| 4 | ( pair ?a ?b ) : ( ?A AND ?B ) -> ( R ?A ) ( ?a : ?A ) ( ?b : ?B ) | |
| 5 | - | ( ?A AND ?B ) : Set -> ( ?A : Set ) ( ?B : Set ) |
| 5 | + | Nat : Set -> True |
| 6 | - | ( pair ?a ?b ) : ( ?A AND ?B ) -> ( ( ?A AND ?B ) : Set ) ( ?a : ?A ) ( ?b : ?B ) |
| 6 | + | |
| 7 | - | ( first ?p ) : ?A -> ?p : ( ?A AND ?B ) |
| 7 | + | ( ?A AND ?B ) : Set -> ( ?A : Set ) ( ?B : Set ) |
| 8 | zero : ?n -> Nat | |
| 9 | ( first ( pair ?a ?b ) ) : ?A -> ( R ?A ( ?b : ?B ) ) ( ?a : ?A ) | |
| 10 | ( Nat ) : Set -> True | |
| 11 | - | Nat : Set -> True |
| 11 | + | |
| 12 | ||
| 13 | - | (s ?n) : Nat -> (?n : Nat) |
| 13 | + | |
| 14 | - | zero : ?n -> zero : Nat |
| 14 | + | (first (pair zero zero)) : Nat |
