Theorem ischoicebasestn ( n : nat ) : ischoicebase (⟦n⟧). Proof. induction n as [ | n IHn ]. - apply ( ischoicebaseempty2 negstn0 ). - apply ( ischoicebaseweqf ( weqdnicoprod n lastelement ) ( ischoicebasecoprod IHn ischoicebaseunit ) ). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.