Entry	Value
Package Name	sum-thm
Count	7
Theorems	ISL_case_sum : !f g x. ISL x ==> case_sum f g x = f (OUTL x) ISR_case_sum : !f g x. ISR x ==> case_sum f g x = g (OUTR x) case_sum_id : !x. case_sum INL INR x = x inl_inj : !a b. INL a = INL b <=> a = b inr_inj : !a b. INR a = INR b <=> a = b sum_CASES : !x. (?a. x = INL a) \/ (?b. x = INR b) sum_distinct : !a b. ~(INL a = INR b)

Back to main package page