fact: Definition nat_less_n_fun' (S : CSetoid) (n : nat) (f : forall i : nat, i <= n -> S) := forall i j : nat, i = j -> forall (H : i <= n) (H' : j <= n), f i H [=] f j H'.
imports: CoRN.tactics.CornTac CoRN.logic.CLogic CoRN.tactics.Step CoRN.algebra.RSetoid