document FC role in unrolling, validate_induct

[Bronsa]

e.g. given

type t = { x : unit list; y : unit list }
let length a = List.length a.x + List.length a.y
let rec g xs =
  match xs.x, xs.y with
  | _::x, y when List.length xs.x > List.length xs.y ->
    Some {x;y}
  | x,_::y ->
    g {x;y}
  | _ -> None

we can do

lemma g_len xs =
  match g xs with
  | None -> true
  | Some xs' ->
    length xs' < length xs
[@@fc] [@@auto]
let rec f xs =
  match g xs with
  | None -> ()
  | Some xs ->
    f xs
[@@measure Ordinal.of_int (length xs)]
[@@disable length]

or

let rec f xs =
  match g xs with
  | None -> ()
  | Some xs ->
    f xs
[@@measure Ordinal.of_int (length xs)]
[@@validate_induct]