zraffer · March 17, 2016 10:35
diff --git a/bool b/bool
 -- #bool
 ∀ (a : #Prop ) → a → a → a
diff --git a/ff b/ff
 -- #ff
 λ (a : #Prop ) → λ (c : a) → λ (d : a) → d
diff --git a/ind_on b/ind_on
 -- #ind_on
 λ (P : #bool → #Prop ) → λ (t : P #tt ) → λ (f : P #ff ) → λ (a : #bool ) → a (P a) t f
diff --git a/ind_on_T b/ind_on_T
 -- #ind_on_T 
 ∀ (P : #bool → #Prop ) → P #tt → P #ff → ∀ (a : #bool ) → P a
diff --git a/ind_on_test b/ind_on_test
 -- #ind_on_test
 (\(t : #ind_on_T ) → t) #ind_on
diff --git a/Prop b/Prop
 -- #Prop
 *
diff --git a/tt b/tt
 -- #tt
 λ (a : #Prop ) → λ (c : a) → λ (d : a) → c
	-- #ind_on
	λ (P : #bool → #Prop ) → λ (t : P #tt ) → λ (f : P #ff ) → λ (a : #bool ) → a (P a) t f
	-- #ind_on_T
	∀ (P : #bool → #Prop ) → P #tt → P #ff → ∀ (a : #bool ) → P a