fact: Definition B1 i := [lsA, s_A] <-$2 A1; lsA1 <- firstn i lsA; a <- nth i lsA defA; lsA2 <- skipn (S i) lsA; incla <- if (lt_dec i (length lsA)) then true else false; ret (a, (incla, lsA1, lsA2, s_A)).
imports: FCF.FCF FCF.CompFold