In the directory lib_sum there is a single file defining the sum type with constructors in1 and in2. Also defined is the case function (essentially the iterator for sum).
** Module lib_sum Imports lib_eq_basics $sum : (Type)->(Type)->Type(sum) $in1_exp : {A:Type}{B:Type}A->sum A B $in2_exp : {A:Type}{B:Type}B->sum A B $sum_elim : {A:Type}{B:Type}{C_sum:(sum A B)->Type} ({x2:A}C_sum (in1_exp A B x2))->({x1:B}C_sum (in2_exp A B x1))-> {z:sum A B}C_sum z sum_double_elim = ... : {A:Type}{B:Type}{T_sum:(sum A B)->(sum A B)->Type} ({x2,x2':A}T_sum (in1_exp A B x2) (in1_exp A B x2'))-> ({x2:A}{x1':B}T_sum (in1_exp A B x2) (in2_exp A B x1'))-> ({x1:B}{x2':A}T_sum (in2_exp A B x1) (in1_exp A B x2'))-> ({x1,x1':B}T_sum (in2_exp A B x1) (in2_exp A B x1'))->{z,z':sum A B} T_sum z z' ** Label (!sum!) sum ** Label (!sum elim!) sum_elim ** Label (!sum in1_exp!) in1_exp ** Label (!sum in2_exp!) in2_exp [[A:Type][B:Type][C_sum:(sum A B)->Type] [f_in1_exp:{x2:A}C_sum (in1_exp A B x2)] [f_in2_exp:{x1:B}C_sum (in2_exp A B x1)][x2:A][x1:B] sum_elim A B C_sum f_in1_exp f_in2_exp (in1_exp A B x2) ==> f_in1_exp x2 || sum_elim A B C_sum f_in1_exp f_in2_exp (in2_exp A B x1) ==> f_in2_exp x1] in1 = ... : {s|Type}{t|Type}s->sum s t in2 = ... : {s|Type}{t|Type}t->sum s t case = ... : {s|Type}{t|Type}{u|Type}(s->u)->(t->u)->(sum s t)->u sum_ind = ... : {s|Type}{t|Type}{P:(sum s t)->Prop}({x:s}P (in1 x))-> ({y:t}P (in2 y))->{z:sum s t}P z is_in1 = ... : {s|Type}{t|Type}(sum s t)->Prop is_in2 = ... : {s|Type}{t|Type}(sum s t)->Prop in1_or_in2 = ... : {s|Type}{t|Type}{x:sum s t}(is_in1 x \/ is_in2 x) in1_not_in2 = ... : {s|Type}{t|Type}{x|s}not (is_in2 (in1|s|t x)) in2_not_in1 = ... : {s|Type}{t|Type}{x|t}not (is_in1 (in2|s|t x)) in1_inj = ... : {s|Type}{t|Type}{x,y:s}(Eq (in1|s|t x) (in1|s|t y))->Eq x y in2_inj = ... : {s|Type}{t|Type}{x,y:t}(Eq (in2|s|t x) (in2|s|t y))->Eq x y