Definition of refinement invariant:

|- ∀a b x_2 x_1 v.
     PAIR_TYPE a b (x_2,x_1) v ⇔
     ∃v1_1 v1_2.
       (v = Conv "Pair" [v1_1; v1_2]) ∧ a x_2 v1_1 ∧ b x_1 v1_2

Definition of refinement invariant:

|- (∀a x_2 x_1 v.
      LIST_TYPE a (x_2::x_1) v ⇔
      ∃v2_1 v2_2.
        (v = Conv "Cons" [v2_1; v2_2]) ∧ a x_2 v2_1 ∧
        LIST_TYPE a x_1 v2_2) ∧
   ∀a v. LIST_TYPE a [] v ⇔ (v = Conv "Nil" [])

Certificate theorem for HD:

|- DeclAssum mini_prelude_decls env ∧ x1 ≠ [] ⇒
   Eval env (Var "HD") ((Eq (LIST_TYPE a) x1 --> a) HD)

Certificate theorem for TL:

|- DeclAssum mini_prelude_decls env ∧ x1 ≠ [] ⇒
   Eval env (Var "TL") ((Eq (LIST_TYPE a) x1 --> LIST_TYPE a) TL)

Certificate theorem for APPEND:

|- DeclAssum mini_prelude_decls env ⇒
   Eval env (Var "APPEND")
     ((LIST_TYPE a --> LIST_TYPE a --> LIST_TYPE a) $++)

Certificate theorem for REV:

|- DeclAssum mini_prelude_decls env ⇒
   Eval env (Var "REV")
     ((LIST_TYPE a --> LIST_TYPE a --> LIST_TYPE a) REV)

Certificate theorem for REVERSE:

|- DeclAssum mini_prelude_decls env ⇒
   Eval env (Var "REVERSE") ((LIST_TYPE a --> LIST_TYPE a) REVERSE)

Definition of declaration list:

|- mini_prelude_decls =
   [Dtype [(["a"; "b"],"prod",[("Pair",[Tvar "a"; Tvar "b"])])];
    Dtype
      [(["a"],"list",
        [("Cons",[Tvar "a"; Tapp [Tvar "a"] "list"]); ("Nil",[])])];
    Dlet (Pvar "HD")
      (Fun "x1"
         (Mat (Var "x1")
            [(Pcon "Nil" [],Raise Bind_error);
             (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v2")]));
    Dlet (Pvar "TL")
      (Fun "x1"
         (Mat (Var "x1")
            [(Pcon "Nil" [],Raise Bind_error);
             (Pcon "Cons" [Pvar "v2"; Pvar "v1"],Var "v1")]));
    Dletrec
      [("APPEND","v3",
        Fun "v4"
          (Mat (Var "v3")
             [(Pcon "Nil" [],Var "v4");
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               Con "Cons"
                 [Var "v2";
                  App Opapp (App Opapp (Var "APPEND") (Var "v1"))
                    (Var "v4")])]))];
    Dletrec
      [("REV","v3",
        Fun "v4"
          (Mat (Var "v3")
             [(Pcon "Nil" [],Var "v4");
              (Pcon "Cons" [Pvar "v2"; Pvar "v1"],
               App Opapp (App Opapp (Var "REV") (Var "v1"))
                 (Con "Cons" [Var "v2"; Var "v4"]))]))];
    Dlet (Pvar "REVERSE")
      (Fun "v1"
         (App Opapp (App Opapp (Var "REV") (Var "v1")) (Con "Nil" [])))]