fact: Definition rec_nat (P : nat -> Type) n (step : forall n, Below_nat P n -> P n) : P n := step n (below_nat P step n).
imports: Bvector Vectors.Vector Equations.Init Equations.CoreTactics Equations.Prop.DepElim Equations.Prop.Tactics Equations.Prop.Constants Equations.Prop.FunctionalInduction