Entry	Value
Package Name	sum-def
Count	10
Theorems	ISL_INL : !a. ISL (INL a) ISL_INR : !b. ~ISL (INR b) ISR_INL : !a. ~ISR (INL a) ISR_INR : !b. ISR (INR b) OUTL : !a. OUTL (INL a) = a OUTR : !b. OUTR (INR b) = b case_sum_left : !f g a. case_sum f g (INL a) = f a case_sum_right : !f g b. case_sum f g (INR b) = g b sum_INDUCT : !p. (!a. p (INL a)) /\ (!b. p (INR b)) ==> (!x. p x) sum_RECURSION : !f g. ?fn. (!a. fn (INL a) = f a) /\ (!b. fn (INR b) = g b)

Back to main package page