module Skeleton
  type skeleton =
    | S0
    | S1 skeleton
    | S2 skeleton skeleton
    | S3 skeleton skeleton skeleton

  let ghost skeleton1 (s: skeleton)
    requires { match s with S1 _ -> true | _ -> false end }
    ensures { match s with S1 s1 -> result = s1 | _ -> false end }
  = match s with S1 s1 -> s1 | _ -> absurd end

  let ghost skeleton2 (s: skeleton)
    requires { match s with S2 _ _ -> true | _ -> false end }
    ensures { match s with S2 s1 s2 -> result = (s1,s2) | _ -> false end }
  = match s with S2 s1 s2 -> (s1,s2) | _ -> absurd end

  let ghost skeleton3 (s: skeleton)
    requires { match s with S3 _ _ _ -> true | _ -> false end }
    ensures { match s with S3 s1 s2 s3 -> result = (s1,s2,s3) | _ -> false end }
  = match s with S3 s1 s2 s3 -> (s1,s2,s3) | _ -> absurd end

  let ghost skeleton12 (s: skeleton)
    requires { match s with S1 _ | S2 _ _ -> true | _ -> false end }
    ensures { match s with S1 s1 | S2 s1 _ -> result = s1 | _ -> false end }
  = match s with S1 s1 | S2 s1 _ -> s1 | _ -> absurd end

  let ghost skeleton123 (s: skeleton)
    requires { match s with S1 _ | S2 _ _ | S3 _ _ _ -> true | _ -> false end }
    ensures { match s with S1 s1 | S2 s1 _ | S3 s1 _ _ -> result = s1 | _ -> false end }
  = match s with S1 s1 | S2 s1 _ | S3 s1 _ _ -> s1 | _ -> absurd end

  let ghost skeleton23 (s: skeleton)
    requires { match s with S2 _ _ | S3 _ _ _ -> true | _ -> false end }
    ensures { match s with S2 s1 s2 | S3 s1 s2 _ -> result = (s1, s2) | _ -> false end }
  = match s with S2 s1 s2 | S3 s1 s2 _ -> (s1, s2) | _ -> absurd end
end