5 lines
169 B
Text
5 lines
169 B
Text
|
and.intro : ?a → ?b → ?a ∧ ?b
|
|||
|
|
or.elim : ?a ∨ ?b → (?a → ?c) → (?b → ?c) → ?c
|
|||
|
|
eq : ?A → ?A → Prop
|
|||
|
|
eq.rec : ?C ?a → (Π {a : ?A}, ?a = a → ?C a)
|