proposition: Lemma fin_lt_n : forall (n : nat) (i : fin n), fin_to_nat i < n.
proof: Proof. intros. funelim (fin_to_nat i). - apply -> PeanoNat.Nat.succ_le_mono; apply PeanoNat.Nat.le_0_l. - apply -> PeanoNat.Nat.succ_lt_mono; assumption. Defined.
imports: Program Equations.Prop.EqDecInstances Equations.Prop.Equations