Definition three_rec {A : UU} (a b c : A) : stn 3 -> A. Proof. induction 1 as [n p]. induction n as [|n _]; [apply a|]. induction n as [|n _]; [apply b|]. induction n as [|n _]; [apply c|]. induction (nopathsfalsetotrue p). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.