The name of the term defined by " (fun x0 : set => fun x1 : set -> ((set -> prop) -> prop) -> (set -> set -> set) -> (set -> prop) -> set -> set => x1 (ap x0 0) (decode_c (ap x0 1)) (decode_b (ap x0 2)) (decode_p (ap x0 3)) (ap x0 4))." is "unpack_c_b_p_e_i".
The name of the term defined by " (fun x0 : set -> set -> prop => forall x1 x2, x0 x1 x2 -> x0 x2 x1)." is "symmetric".
The name of the term defined by " (fun x0 : set => pack_b (Sep (setexp x0 x0) (fun x1 : set => bij x0 x0 (ap x1))) (fun x1 x2 : set => lam x0 (fun x3 : set => ap x2 (ap x1 x3))))." is "symgroup".
The name of the term defined by " (fun x0 : set => Eps_i (fun x1 : set => and (ordinal x1) (SNo_ x1 x0)))." is "SNoLev".
The name of the term defined by " (fun x0 : set => fun x1 : set -> prop => lam 2 (fun x2 : set => If_i (x2 = 0) x0 (Sep x0 x1)))." is "pack_p".
The name of the term defined by " (fun x0 : set => and (Group x0) (forall x1, x1 :e ap x0 0 -> (forall x2, x2 :e ap x0 0 -> x1 = x2)))." is "trivial_Group_p".
The name of the term defined by " (fun x0 : set => fun x1 : set -> (set -> set) -> (set -> set) -> set -> set -> set => x1 (ap x0 0) (ap (ap x0 1)) (ap (ap x0 2)) (ap x0 3) (ap x0 4))." is "unpack_u_u_e_e_i".
The name of the term defined by " ordsucc u25." is "u26".
The name of the term defined by " (fun x0 : set => fun x1 : set -> set -> set -> set => x1 (ap x0 0) (ap x0 1) (ap x0 2))." is "unpack_e_e_i".
The name of the term defined by " ordsucc u45." is "u46".