Definition isolfun3 {X Y:UU} (x1 x2 x3:X) (i1 : isisolated _ x1) (i2 : isisolated _ x2) (i3 : isisolated _ x3) (y1 y2 y3 y':Y) : X → Y. Proof. intros x. induction (i1 x). - exact y1. - induction (i2 x). + exact y2. + induction (i3 x). * exact y3. * exact y'. Defined.