{n} : forall (f : Fin (n.+2) -> Type) {dprop : forall i, Decidable (f i)} (left_true : f fin_zero) (right_false : ~ f fin_last), {k : Fin n.+1 & f (fin_incl k) /\ ~ f (fsucc k)}. Proof. intros ???. destruct n as [|n]. - exists fin_zero. split; assumption. - destruct (dec (f (fin_incl fin_last))) as [prev_true|prev_false]. + exists fin_last. split; assumption. + destruct ( _ (f o fin_incl) _ left_true prev_false) as [k' [fleft fright]]. exists (fin_incl k'). split; assumption. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.