Definition three_rec_dep (P : three -> UU): P (● 0) -> P (● 1) -> P (● 2) -> ∏ n, P n. Proof. intros a b c n. induction n as [n p]. induction n as [|n _]. eapply stn_predicate. apply a. induction n as [|n _]. eapply stn_predicate. apply b. induction n as [|n _]. eapply stn_predicate. apply c. induction (nopathsfalsetotrue p). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.