fact: Definition rec_fin (P : forall n, fin n -> Type) {n} v (step : forall n (v : fin n), Below_fin P v -> P n v) : P n v := step n v (below_fin P step v).
imports: Program.Basics Program.Combinators Equations(Equations)