diff --git a/Strata/Languages/Python/BoogieTypePrelude.lean b/Strata/Languages/Python/BoogieTypePrelude.lean
new file mode 100644
index 000000000..3270e9626
--- /dev/null
+++ b/Strata/Languages/Python/BoogieTypePrelude.lean
@@ -0,0 +1,827 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DDM.Elab
+import Strata.DDM.AST
+import Strata.Languages.Boogie.DDMTransform.Parse
+import Strata.Languages.Boogie.Verifier
+
+namespace Strata
+
+def boogieTypePrelude :=
+#strata
+program Boogie;
+
+//Generic tag for List
+type List_tag;
+const CONS : List_tag;
+const NIL : List_tag;
+axiom [list_tag_unique]: CONS != NIL;
+axiom [all_list_tag]: forall lt: List_tag :: lt == CONS || lt == NIL;
+
+type Error;
+
+// Constructors
+function Error_TypeError (msg : string) : Error;
+function Error_AttributeError (msg : string) : Error;
+function Error_RePatternError (msg : string) : Error;
+function Error_Unimplemented (msg : string) : Error;
+function Error_Undefined (msg : string) : Error;
+
+type Error_tag;
+const TYPEERR : Error_tag;
+const ATRERR : Error_tag;
+const REERR : Error_tag;
+const UNIMPLERR : Error_tag;
+const UNDEFERR : Error_tag;
+axiom [error_tag_unique]: TYPEERR != ATRERR && TYPEERR != REERR && TYPEERR != UNIMPLERR && TYPEERR != UNDEFERR &&
+                          ATRERR != REERR && ATRERR != UNIMPLERR && ATRERR != UNDEFERR &&
+                          REERR != UNIMPLERR && REERR != UNDEFERR &&
+                          UNIMPLERR != UNDEFERR ;
+
+axiom [all_error_tag]: forall et: Error_tag :: et == TYPEERR || et == ATRERR || et == REERR || et == UNIMPLERR || et == UNDEFERR;
+
+function ErrorTag (e: Error) : Error_tag;
+axiom [ErrorTag_def_typeerr]: forall msg: string :: {ErrorTag(Error_TypeError(msg))} ErrorTag(Error_TypeError(msg)) == TYPEERR;
+axiom [ErrorTag_def_attrerr]: forall msg: string :: {ErrorTag(Error_AttributeError(msg))} ErrorTag(Error_AttributeError(msg)) == ATRERR;
+axiom [ErrorTag_def_reerr]: forall msg: string :: {ErrorTag(Error_RePatternError(msg))} ErrorTag(Error_RePatternError(msg)) == REERR;
+axiom [ErrorTag_def_unimplerr]: forall msg: string :: {ErrorTag(Error_Unimplemented(msg))} ErrorTag(Error_Unimplemented(msg)) == UNIMPLERR;
+axiom [ErrorTag_def_undeferr]: forall msg: string :: {ErrorTag(Error_Undefined(msg))} ErrorTag(Error_Undefined(msg)) == UNDEFERR;
+
+type Except_tag;
+const OK : Except_tag;
+const ERR : Except_tag;
+axiom [except_tag_unique]: OK != ERR;
+axiom [all_except_tag]: forall et: Except_tag :: et == OK || et == ERR;
+
+type stringExcept;
+function stringExcept_ok (s: string): stringExcept;
+function stringExcept_err (e: Error): stringExcept;
+function stringExcept_tag (ie: stringExcept) : Except_tag;
+axiom [stringExcept_tag_ok_def]: forall s: string :: {stringExcept_tag(stringExcept_ok(s))}
+  stringExcept_tag(stringExcept_ok(s)) == OK;
+axiom [stringExcept_tag_err_def]: forall e: Error :: {stringExcept_tag(stringExcept_err(e))}
+  stringExcept_tag(stringExcept_err(e)) == ERR;
+function stringExcept_unwrap (lie: stringExcept) : string;
+axiom [stringExcept_unwrap_def]: forall s: string :: {stringExcept_tag(stringExcept_ok(s))}
+  stringExcept_unwrap(stringExcept_ok(s)) == s;
+
+type boolExcept;
+function boolExcept_ok (b: bool): boolExcept;
+function boolExcept_err (e: Error): boolExcept;
+function boolExcept_tag (be: boolExcept) : Except_tag;
+axiom [boolExcept_tag_ok_def]: forall b: bool :: {boolExcept_tag(boolExcept_ok(b))}
+  boolExcept_tag(boolExcept_ok(b)) == OK;
+axiom [boolExcept_tag_err_def]: forall e: Error :: {boolExcept_tag(boolExcept_err(e))}
+  boolExcept_tag(boolExcept_err(e)) == ERR;
+function boolExcept_unwrap (lie: boolExcept) : bool;
+axiom [boolExcept_unwrap_def]: forall b: bool :: {boolExcept_tag(boolExcept_ok(b))}
+  boolExcept_unwrap(boolExcept_ok(b)) == b;
+
+type intExcept;
+function intExcept_ok (i: int): intExcept;
+function intExcept_err (e: Error): intExcept;
+function intExcept_tag (ie: intExcept) : Except_tag;
+axiom [intExcept_tag_ok_def]: forall i: int :: {intExcept_tag(intExcept_ok(i))}
+  intExcept_tag(intExcept_ok(i)) == OK;
+axiom [intExcept_tag_err_def]: forall e: Error :: {intExcept_tag(intExcept_err(e))}
+  intExcept_tag(intExcept_err(e)) == ERR;
+function intExcept_unwrap (lie: intExcept) : int;
+axiom [intExcept_unwrap_def]: forall i: int :: {intExcept_tag(intExcept_ok(i))}
+  intExcept_unwrap(intExcept_ok(i)) == i;
+
+type Datetime;
+
+// Value and ListValue types
+type Value;
+type ListValue;
+
+type ValueExcept;
+function ValueExcept_ok (v: Value): ValueExcept;
+function ValueExcept_err (e: Error): ValueExcept;
+function ValueExcept_tag (ve: ValueExcept) : Except_tag;
+axiom [ValueExcept_tag_ok_def]: forall v: Value :: {ValueExcept_tag(ValueExcept_ok(v))}
+  ValueExcept_tag(ValueExcept_ok(v)) == OK;
+axiom [ValueExcept_tag_err_def]: forall e: Error :: {ValueExcept_tag(ValueExcept_err(e))}
+  ValueExcept_tag(ValueExcept_err(e)) == ERR;
+function ValueExcept_unwrap (lve: ValueExcept) : Value;
+axiom [ValueExcept_unwrap_def]: forall v: Value :: {ValueExcept_tag(ValueExcept_ok(v))}
+  ValueExcept_unwrap(ValueExcept_ok(v)) == v;
+
+// Class type
+type InstanceAttributes := Map string ValueExcept;
+type ClassInstance;
+
+// Constructors
+function Value_bool (b : bool) : Value;
+function Value_int (i : int) : Value;
+function Value_float (f : real) : Value;
+function Value_str (s : string) : Value;
+function Value_datetime (d : Datetime) : Value;
+function Value_none() : Value;
+function Value_list (lv : ListValue) : Value;
+function Value_class (ci: ClassInstance) : Value;
+
+function ListValue_nil() : ListValue;
+function ListValue_cons(x0 : Value, x1 : ListValue) : ListValue;
+//Tags
+function ListValue_tag (l: ListValue) : List_tag;
+axiom [ListValue_tag_nil_def]: ListValue_tag (ListValue_nil()) == NIL;
+axiom [ListValue_tag_cons_def]: forall v: Value, vs: ListValue ::{ListValue_cons(v, vs)} ListValue_tag (ListValue_cons(v, vs)) == CONS;
+
+// Types of Value
+type ValueType;
+type ListValueType;
+const BOOL : ValueType;
+const INT : ValueType;
+const FLOAT : ValueType;
+const STR : ValueType;
+const DATETIME : ValueType;
+const NONE : ValueType;
+function ValueType_class(classname: string): ValueType;
+
+function isListValueType (t: ValueType): bool;
+function isClassValueType (t: ValueType): bool;
+axiom [isClassType_def]: forall c: string :: {isClassValueType(ValueType_class(c))} isClassValueType(ValueType_class(c));
+
+//Uniqueness axioms
+axiom [unique_ValueType_DATETIME]: DATETIME != BOOL && DATETIME != INT && DATETIME != FLOAT && DATETIME != STR && DATETIME != NONE && !isListValueType(DATETIME) && !(isClassValueType(DATETIME));
+axiom [unique_ValueType_bool]: BOOL != INT && BOOL != FLOAT && BOOL != STR && BOOL != NONE && !isListValueType(BOOL) && !(isClassValueType(BOOL));
+axiom [unique_ValueType_int]: INT != STR && INT != FLOAT && INT != NONE && !isListValueType(INT) && !(isClassValueType(INT));
+axiom [unique_ValueType_float]: FLOAT != STR && FLOAT != NONE && !isListValueType(FLOAT) && !(isClassValueType(FLOAT));
+axiom [unique_ValueType_str]: STR != NONE && !isListValueType(STR) && !(isClassValueType(STR));
+axiom [unique_ValueType_none]: !isListValueType(NONE) && !(isClassValueType(NONE));
+axiom [classtype_ne_listtype]: forall t: ValueType :: {isListValueType (t), isClassValueType (t)} !(isListValueType (t) && isClassValueType (t));
+axiom [all_ValueType_cases]: forall t: ValueType ::
+  t == BOOL ||
+  t == INT ||
+  t == FLOAT ||
+  t == STR ||
+  t == NONE ||
+  t == DATETIME ||
+  isListValueType (t) ||
+  isClassValueType (t);
+
+//Eq axioms
+axiom [value_int_eq]: forall i: int, j: int :: {Value_int(i) == Value_int(j)} (Value_int(i) == Value_int(j)) == (i == j);
+axiom [value_bool_eq]: forall b1: bool, b2: bool :: {Value_bool(b1) == Value_bool(b2)} (Value_bool(b1) == Value_bool(b2)) == (b1 == b2);
+axiom [value_float_eq]: forall r1: real, r2: real :: {Value_float(r1) == Value_float(r2)} (Value_float(r1) == Value_float(r2)) == (r1 == r2);
+axiom [value_str_eq]: forall s1: string, s2: string :: {Value_str(s1) == Value_str(s2)} (Value_str(s1) == Value_str(s2)) == (s1 == s2);
+axiom [value_datetime_eq]: forall d1: Datetime, d2: Datetime :: {Value_datetime(d1) == Value_datetime(d2)} (Value_datetime(d1) == Value_datetime(d2)) == (d1 == d2);
+
+//Constructors and tag functions of ListType
+function ListType_nil() : (ListValueType);
+function ListType_cons(x0 : ValueType, x1 : ListValueType) : ListValueType;
+function ValueType_List (l: ListValueType) : ValueType;
+function ListValueType_tag (l: ListValueType) : List_tag;
+axiom [ListValueType_tag_nil_def]: ListValueType_tag (ListType_nil()) == NIL;
+axiom [ListValueType_tag_cons_def]: forall t: ValueType, ts: ListValueType ::{ListType_cons(t, ts)} (ListValueType_tag (ListType_cons(t, ts)) == CONS);
+axiom [isListValueType_def]: forall l: ListValueType ::{isListValueType(ValueType_List (l))} isListValueType(ValueType_List (l));
+
+// TypeOf and TypesOf functions
+function TypeOf (v : Value) : ValueType;
+function TypesOf (v: ListValue) : ListValueType;
+// Definitions
+axiom [TypesOf_nil_def]: TypesOf(ListValue_nil()) == ListType_nil();
+axiom [TypesOf_cons_def]: forall v: Value, vs: ListValue ::{ListValue_cons(v, vs)} TypesOf(ListValue_cons(v, vs)) == ListType_cons(TypeOf(v), TypesOf(vs));
+axiom [TypeOf_list_def]: forall l: ListValue ::{Value_list(l)} TypeOf(Value_list(l)) ==  ValueType_List(TypesOf(l));
+axiom [TypeOf_bool]: forall b: bool :: {TypeOf(Value_bool(b))} TypeOf(Value_bool(b)) == BOOL;
+axiom [TypeOf_int]: forall i: int :: {Value_int(i)} TypeOf(Value_int(i)) == INT;
+axiom [TypeOf_float]: forall f: real :: {Value_float(f)} TypeOf(Value_float(f)) == FLOAT;
+axiom [TypeOf_str]: forall s: string :: {Value_str(s)} TypeOf(Value_str(s)) == STR;
+axiom [TypeOf_datetime]: forall d: Datetime :: {Value_datetime(d)} TypeOf(Value_datetime(d)) == DATETIME;
+axiom [TypeOf_none]: TypeOf(Value_none()) == NONE;
+axiom [TypeOf_list]: forall l: ListValue :: {Value_list(l)} TypeOf(Value_list(l)) == ValueType_List(TypesOf(l));
+
+axiom [TypeOf_bool_exists]: forall v: Value :: {TypeOf(v) == BOOL} TypeOf(v) == BOOL ==> exists b: bool :: v == Value_bool(b);
+axiom [TypeOf_int_exists]: forall v: Value :: {TypeOf(v) == INT} TypeOf(v) == INT ==> exists i: int :: v == Value_int(i);
+axiom [TypeOf_float_exists]: forall v: Value :: {TypeOf(v) == FLOAT} TypeOf(v) == FLOAT ==> exists r: real :: v == Value_float(r);
+axiom [TypeOf_string_exists]: forall v: Value :: {TypeOf(v) == STR} TypeOf(v) == STR ==> exists s: string :: v == Value_str(s);
+axiom [TypeOf_none']: forall v: Value :: {TypeOf(v) == NONE} (TypeOf(v) == NONE) == (v == Value_none()) ;
+
+function isBool (v: Value): bool {
+  TypeOf(v) == BOOL
+}
+function isInt (v: Value): bool {
+  TypeOf(v) == INT
+}
+function isStr (v: Value): bool {
+  TypeOf(v) == STR
+}
+function isFloat (v: Value): bool{
+  TypeOf(v) == FLOAT
+}
+function isNone (v: Value): bool{
+  TypeOf(v) == NONE
+}
+function isDatetime (v: Value): bool{
+  TypeOf(v) == DATETIME
+}
+
+function isList (v: Value): bool;
+function isClassInstance (v: Value): bool;
+
+axiom [isList_def]: forall l: ListValue :: {Value_list(l)} isList(Value_list(l));
+axiom [isList_def']: forall v: Value :: {isListValueType(TypeOf(v))} isList(v) == isListValueType(TypeOf(v));
+axiom [isClassInstance_def]: forall ci: ClassInstance :: {Value_class(ci)} isClassInstance(Value_class(ci));
+axiom [isClassInstance_def']: forall v: Value :: {isClassValueType(TypeOf(v))} isClassInstance(v) == isClassValueType(TypeOf(v));
+
+axiom [TypeOf_list_exists]: forall v: Value :: {isList(v)} isList(v) ==> exists l: ListValue :: v == Value_list(l);
+axiom [TypeOf_class_exists]: forall v: Value :: {isClassInstance(v)} isClassInstance(v) ==> exists ci: ClassInstance :: v == Value_class(ci);
+
+
+//Casting
+function as_bool (v: Value) : bool;
+axiom [as_bool_def]: forall b: bool :: {as_bool(Value_bool(b))} as_bool(Value_bool(b)) == b;
+
+// isSubType functions
+function isSubType (t1: ValueType, t2: ValueType) : bool;
+function isSubTypes (t1: ListValueType, t2: ListValueType) : bool;
+//Definitions
+axiom [isSubTypes_nil_def]: isSubTypes(ListType_nil(), ListType_nil());
+axiom [not_isSubTypes_nil]: forall ty: ValueType, l: ListValueType :: !isSubTypes(ListType_nil(), ListType_cons(ty,l));
+axiom [not_isSubTypes_nil']: forall ty: ValueType, l: ListValueType :: !isSubTypes(ListType_cons(ty,l), ListType_nil());
+axiom [isSubTypes_cons_def]:forall t: ValueType, ts: ListValueType, t': ValueType, ts': ListValueType  ::{ListType_cons(t, ts), ListType_cons(t', ts')}
+  isSubTypes(ListType_cons(t, ts), ListType_cons(t', ts')) == (isSubType(t, t') && isSubTypes(ts, ts'));
+axiom [isSubType_list_def]: forall l: ListValueType, l': ListValueType :: {ValueType_List(l), ValueType_List(l')}
+  isSubType(ValueType_List(l), ValueType_List(l')) == isSubTypes(l, l');
+axiom [bool_substype_int]: isSubType(BOOL, INT);
+axiom [int_substype_float]: isSubType(INT, FLOAT);
+axiom [not_isSubstype_string]: forall t: ValueType ::{isSubType(STR, t), isSubType(t,STR)}
+  t == STR || (!isSubType(STR, t) && !isSubType(t,STR));
+axiom [not_isSubstype_none]: forall t: ValueType ::{isSubType(NONE, t), isSubType(NONE, t)}
+  t == NONE || (!isSubType(NONE, t) && !isSubType(t,NONE));
+axiom [not_isSubstype_list]: forall t: ValueType, t': ValueType ::{isSubType(t, t')}
+  ((isListValueType(t) && !isListValueType(t')) || (!isListValueType(t) && isListValueType(t'))) ==> (!isSubType(t, t') && !isSubType(t', t));
+axiom [not_isSubstype_class_othertypes]: forall t: ValueType, t': ValueType ::{isSubType(t, t')}
+  ((isClassValueType(t) && !isClassValueType(t')) || (!isClassValueType(t) && isClassValueType(t'))) ==> (!isSubType(t, t') && !isSubType(t', t));
+axiom [not_isSubstype_class]: forall t: ValueType, c: string ::{isSubType(ValueType_class(c), t), isSubType(t,ValueType_class(c))}
+  t != ValueType_class(c) ==> (!isSubType(ValueType_class(c), t) && !isSubType(t,ValueType_class(c)));
+// Supporting lemmas
+axiom [isSubtype_rfl]: forall t: ValueType::{isSubType (t,t)} isSubType (t,t);
+axiom [isSubtype_mono]: forall t1: ValueType, t2: ValueType ::{isSubType (t1,t2)} !isSubType (t1,t2) || (t1 == t2 || !isSubType(t2,t1));
+axiom [isSubtype_trans]: forall t1: ValueType, t2: ValueType, t3: ValueType::{isSubType(t1, t2)} !(isSubType(t1, t2) && isSubType(t2, t3)) || isSubType(t1, t3);
+
+// isInstance function:
+function isInstance (v: Value, vt: ValueType) : bool {
+  isSubType(TypeOf(v), vt)
+}
+
+function isInstance_ofBool (v: Value): bool {
+  isInstance(v, BOOL)
+}
+
+function isInstance_ofInt (v: Value): bool {
+  isInstance(v, INT)
+}
+
+function isInstance_ofFloat (v: Value): bool {
+  isInstance(v, FLOAT)
+}
+
+function isInstance_ofStr (v: Value): bool {
+  isInstance(v, STR)
+}
+
+
+function is_IntReal (v: Value) : bool;
+function Value_real_to_int (v: Value) : int;
+// to be extended
+function normalize_value (v : Value) : Value {
+  if v == Value_bool(true) then Value_int(1)
+  else (if v == Value_bool(false) then Value_int(0) else
+        if TypeOf(v) == FLOAT && is_IntReal(v) then Value_int(Value_real_to_int(v)) else
+        v)
+}
+
+type ListValueExcept;
+function ListValueExcept_ok (l: ListValue): ListValueExcept;
+function ListValueExcept_err (e: Error): ListValueExcept;
+function ListValueExcept_tag (lve: ListValueExcept) : Except_tag;
+axiom [ListValueExcept_tag_ok_def]: forall l: ListValue :: {ListValueExcept_tag(ListValueExcept_ok(l))}
+  ListValueExcept_tag(ListValueExcept_ok(l)) == OK;
+axiom [ListValueExcept_tag_err_def]: forall e: Error :: {ListValueExcept_tag(ListValueExcept_err(e))}
+  ListValueExcept_tag(ListValueExcept_err(e)) == ERR;
+function ListValueExcept_unwrap (lve: ListValueExcept) : ListValue;
+axiom [ListValueExcept_unwrap_def]: forall l: ListValue :: {ListValueExcept_tag(ListValueExcept_ok(l))}
+  ListValueExcept_unwrap(ListValueExcept_ok(l)) == l;
+
+// ListValue functions
+function List_contains (l : ListValue, x: Value) : bool;
+function List_len (l : ListValue) : int;
+function List_extend (l1 : ListValue, l2: ListValue) : ListValue;
+function List_append (l: ListValue, x: Value) : ListValue;
+function List_get (l : ListValue, i : int) : ValueExcept;
+function List_reverse (l: ListValue) : ListValue;
+function List_index! (l: ListValue, v: Value): int;
+function List_index (l: ListValue, v: Value): intExcept;
+function List_repeat (l: ListValue, n: int): ListValue;
+function List_insert (l: ListValue, i: int, v: Value): ListValue;
+function List_remove (l: ListValue, v: Value): ListValue;
+//TO BE done
+function List_pop (l: ListValue, i: int): ListValueExcept;
+
+//List function axioms
+axiom [List_contains_nil_def]: forall x : Value ::{List_contains(ListValue_nil(), x)}
+  !List_contains(ListValue_nil(), x);
+axiom [List_contains_cons_def]: forall x : Value, h : Value, t : ListValue ::{List_contains(ListValue_cons(h,t),x)}
+  List_contains(ListValue_cons(h,t),x) == ((normalize_value(x)==normalize_value(h)) || List_contains(t, x));
+
+axiom [List_len_nil_def]: List_len (ListValue_nil()) == 0;
+axiom [List_len_cons_def]: forall h : Value, t : ListValue ::{List_len (ListValue_cons(h,t))}
+  List_len (ListValue_cons(h,t)) == 1 + List_len(t);
+axiom [List_len_nonneg]: forall l: ListValue :: {List_len(l)} List_len(l) >= 0 ;
+axiom [List_nil_of_len_zero]: forall l: ListValue :: {List_len(l) == 0}
+  (List_len(l) == 0) == (l == ListValue_nil());
+
+axiom [List_extend_nil_def]: forall l1: ListValue ::{List_extend (l1, ListValue_nil())}
+  List_extend (l1, ListValue_nil()) == l1;
+axiom [List_nil_extend_def]: forall l1: ListValue ::{List_extend (ListValue_nil(), l1)}
+  List_extend (ListValue_nil(), l1) == l1;
+axiom [List_cons_extend_def]: forall h: Value, t: ListValue, l2: ListValue  ::{List_extend (ListValue_cons(h,t), l2)}
+  List_extend (ListValue_cons(h,t), l2) == ListValue_cons(h, List_extend(t,l2));
+
+axiom [List_cons_extend_contains]: forall x: Value, l1: ListValue, l2: ListValue  ::{List_contains (List_extend(l1,l2), x)}
+  List_contains (List_extend(l1,l2), x) == (List_contains (l1,x) || List_contains(l2,x));
+axiom [List_len_extend]: forall l1: ListValue, l2: ListValue  ::{List_len (List_extend(l1,l2))}
+  List_len (List_extend(l1,l2)) == List_len (l1) + List_len(l2);
+axiom [List_extend_assoc]: forall l1: ListValue, l2: ListValue, l3: ListValue :: {List_extend(List_extend(l1,l2), l3)}
+  List_extend(List_extend(l1,l2), l3) == List_extend(l1,List_extend(l2,l3));
+
+axiom [List_get_nil]: forall i : int ::{List_get (ListValue_nil(), i)}
+  List_get (ListValue_nil(), i) == ValueExcept_err(Error_Undefined("index out of bound"));
+axiom [List_get_zero]: forall h : Value, t : ListValue ::{List_get (ListValue_cons(h,t), 0)}
+  List_get (ListValue_cons(h,t), 0) == ValueExcept_ok(h);
+axiom [List_get_ind]: forall h : Value, t : ListValue, i : int ::{List_get (ListValue_cons(h,t), i)}
+  (i > 0) ==> (List_get (ListValue_cons(h,t), i)) == List_get (t, i - 1);
+axiom [List_get_contains]: forall l: ListValue, i: int, x: Value :: {List_contains(l,x), List_get(l,i)}
+  (List_get(l,i) == ValueExcept_ok(x)) ==> List_contains(l,x);
+axiom [List_get_contains_eq]: forall l: ListValue, x: Value :: {List_contains(l,x)}
+  List_contains(l,x) == (exists i:int :: {} List_get(l,i) == ValueExcept_ok(x));
+axiom [List_get_ok]: forall l: ListValue, i: int:: {List_get(l,i)}
+  ((List_get(l,i)) != ValueExcept_err(Error_Undefined("index out of bound"))) == (i < List_len(l) && i >= 0);
+axiom [List_get_ok']: forall l: ListValue, i: int:: {List_get(l,i)}
+  (ValueExcept_tag(List_get(l,i)) != ERR) == (i < List_len(l) && i >= 0);
+axiom [List_extend_get]: forall l1: ListValue, l2: ListValue, i: int :: {List_get(List_extend(l1,l2), i)}
+  List_get(List_extend(l1,l2), i) == if i < List_len(l1) then List_get(l1, i) else List_get(l2, i - List_len(l1));
+
+axiom [List_append_def]: forall l: ListValue, x: Value :: {List_append(l,x)}
+  List_append(l,x) == List_extend(l, ListValue_cons(x, ListValue_nil()));
+
+axiom [List_reverse_def_nil]: List_reverse(ListValue_nil()) == ListValue_nil();
+axiom [List_reverse_def_cons]: forall h: Value, t: ListValue:: {List_reverse(ListValue_cons(h,t))}
+  List_reverse(ListValue_cons(h,t)) == List_append(List_reverse(t), h);
+axiom [List_reverse_len]: forall l: ListValue :: {List_len(List_reverse(l))}
+  List_len(l) == List_len(List_reverse(l));
+axiom [List_reverse_contain]: forall l: ListValue, v: Value :: {List_contains (List_reverse(l), v)}
+  List_contains (List_reverse(l), v) == List_contains(l,v);
+axiom [List_reverse_index]: forall l: ListValue, i: int :: {List_get(List_reverse(l), i)}
+  List_get(List_reverse(l), i) == List_get(l, List_len(l)-1-i);
+axiom [List_reverse_reverse]: forall l: ListValue :: {List_reverse(List_reverse(l))}
+  List_reverse(List_reverse(l)) == l;
+axiom [List_reverse_extend]: forall l1: ListValue, l2: ListValue :: {List_reverse(List_extend(l1,l2))}
+  List_reverse(List_extend(l1,l2)) == List_extend(List_reverse(l2), List_reverse(l1));
+
+axiom [List_index!_nil_def]: forall v: Value :: {List_index!(ListValue_nil(), v)}
+  List_index!(ListValue_nil(), v) == 0;
+axiom [List_index!_cons_def_1]: forall h: Value, t: ListValue :: {List_index!(ListValue_cons(h,t), h)}
+  List_index!(ListValue_cons(h,t), h) == 0;
+axiom [List_index!_cons_def_2]: forall v: Value, h: Value, t: ListValue :: {List_index!(ListValue_cons(h,t), v)}
+  !(normalize_value(v)==normalize_value(h)) ==> List_index!(ListValue_cons(h,t), v) == List_index!(t, v) + 1;
+axiom [List_index_def]: forall v: Value, l: ListValue :: {List_index(l, v)}
+  List_index(l,v) ==  if (List_index!(l,v) == List_len(l)) then intExcept_err(Error_Undefined("List does not contain element"))
+                      else intExcept_ok(List_index!(l,v));
+
+axiom [List_repeat_def]: forall l: ListValue, n: int :: {List_repeat(l, n)}
+  List_repeat(l, n) ==  if (n <= 0) then ListValue_nil() else
+                        if (n == 1) then l else  List_extend(l, List_repeat(l, n-1));
+axiom [List_repeat_mul]: forall l: ListValue, n: int, m: int :: {List_repeat(List_repeat(l, n),m)}
+  List_repeat(List_repeat(l, n),m) == List_repeat(l, n * m);
+axiom [List_repeat_len]: forall l: ListValue, n: int :: {List_len(List_repeat(l, n))}
+  n > 0 ==> List_len(List_repeat(l, n)) == n * List_len(l);
+axiom [List_repeat_contain]: forall l: ListValue, v: Value, n: int :: {List_contains(List_repeat(l, n), v)}
+  n > 0 ==> (List_contains(List_repeat(l, n), v) == List_contains(l, v));
+axiom [List_repeat_get]: forall l: ListValue, v: Value, i: int, n: int, m: int :: {List_get(List_repeat(l, n), i + m * List_len(l))}
+  (i >= 0 && i < List_len(l) && m >= 0 && m < n) ==> (List_get(List_repeat(l, n), i + m * List_len(l)) == List_get(l, i));
+
+axiom [List_insert_def0]: forall i: int, v: Value :: {List_insert(ListValue_nil(), i, v)}
+  List_insert(ListValue_nil(), i, v) == ListValue_cons(v, ListValue_nil());
+axiom [List_insert_def1]: forall l: ListValue, i: int, v: Value :: {List_insert(l, i, v)}
+  i <= 0 ==> List_insert(l, i, v) == ListValue_cons(v, l);
+axiom [List_insert_def2]: forall h: Value, t: ListValue, i: int, v: Value :: {List_insert(ListValue_cons(h,t), i, v)}
+  (i > 0) ==> List_insert(ListValue_cons(h,t), i, v) == ListValue_cons(h, List_insert(t, i-1, v));
+axiom [List_insert_len]: forall l: ListValue, i: int, v: Value :: {List_len(List_insert(l, i, v))}
+  List_len(List_insert(l, i, v)) == List_len(l) + 1;
+axiom [List_insert_get0]: forall l: ListValue, p: int, v: Value:: {List_get(List_insert(l, p, v), p)}
+  (p >= 0 && p < List_len(l)) ==> (List_get(List_insert(l, p, v), p) == ValueExcept_ok(v));
+axiom [List_insert_get1]: forall l: ListValue, p: int, v: Value:: {List_get(List_insert(l, p, v), p)}
+  p >= List_len(l) ==> (List_get(List_insert(l, p, v), List_len(l)) == ValueExcept_ok(v));
+axiom [List_insert_get2]: forall l: ListValue, p: int, v: Value, i: int :: {List_get(List_insert(l, p, v), i)}
+  (p >= List_len(l) && i < List_len(l)) ==> (List_get(List_insert(l, p, v),i) == List_get(l, i));
+axiom [List_insert_get3]: forall l: ListValue, p: int, v: Value, i: int:: {List_get(List_insert(l, p, v), i)}
+  (p >= 0 && p < List_len(l) && i < p) ==> (List_get(List_insert(l, p, v), i) == List_get(l,i));
+axiom [List_insert_get4]: forall l: ListValue, p: int, v: Value, i: int:: {List_get(List_insert(l, p, v), i)}
+  (p >= 0 && p < List_len(l) && i > p) ==> (List_get(List_insert(l, p, v), i) == List_get(l,i -1));
+axiom [List_insert_get6]: forall l: ListValue, p: int, v: Value, i: int:: {List_get(List_insert(l, p, v), i)}
+  (p <= 0 && i > 0) ==> (List_get(List_insert(l, p, v), i) == List_get(l,i -1));
+axiom [List_insert_contains]: forall l: ListValue, i: int, v: Value :: {List_contains(List_insert(l,i,v),v)}
+  List_contains(List_insert(l,i,v),v);
+
+axiom [List_remove_nil_def]: forall x : Value ::{List_remove(ListValue_nil(), x)}
+  List_remove(ListValue_nil(), x) == ListValue_nil();
+axiom [List_remove_cons_def]: forall x : Value, h : Value, t : ListValue ::{List_remove(ListValue_cons(h,t),x)}
+  List_remove(ListValue_cons(h,t),x) == if (normalize_value(x)==normalize_value(h)) then t
+                                        else ListValue_cons(h, List_remove(t, x));
+axiom [List_remove_len]: forall l: ListValue, x: Value :: {List_len(List_remove(l,x))}
+  List_len(List_remove(l,x)) == if (List_contains(l,x)) then (List_len(l) - 1) else List_len(l);
+axiom [List_remove_not_contain]: forall l: ListValue, x: Value :: {List_remove(l,x)}
+  (!List_contains(l,x)) == (List_remove(l,x) == l);
+
+axiom [List_pop_def0]: forall i: int :: {List_pop(ListValue_nil(), i)}
+  List_pop(ListValue_nil(), i) == ListValueExcept_err(Error_Undefined("Pop from empty list"));
+axiom [List_pop_def1]: forall h: Value, t: ListValue:: {List_pop(ListValue_cons(h,t), 0)}
+  List_pop(ListValue_cons(h,t), 0) == ListValueExcept_ok(t);
+axiom [List_pop_def2]: forall h: Value, t: ListValue, i: int :: {List_pop(ListValue_cons(h,t), i)}
+   List_pop(ListValue_cons(h,t), i) ==
+    if (i > 0 && i <= List_len(t)) then
+        ListValueExcept_ok(ListValue_cons(h, ListValueExcept_unwrap(List_pop(t, i-1))))
+    else ListValueExcept_err(Error_Undefined("Pop outside of index range"));
+axiom [List_pop_def3]: forall h: Value, t: ListValue, i: int :: {List_pop(ListValue_cons(h,t), i)}
+  (i < 0) ==> List_pop(ListValue_cons(h,t), i) == ListValueExcept_err(Error_Undefined("Pop outside of index range"));
+axiom [List_pop_len]: forall l: ListValue, i: int :: {List_len(ListValueExcept_unwrap(List_pop(l, i)))}
+  List_len(ListValueExcept_unwrap(List_pop(l, i))) == List_len(l) - 1;
+axiom [List_pop_get0]: forall l: ListValue, p: int, i :int:: {List_get(ListValueExcept_unwrap(List_pop(l, p)), i)}
+  (p >= 0 && p < List_len(l) && i < p) ==>
+  (List_get(ListValueExcept_unwrap(List_pop(l, p)), i) == List_get(l, i));
+axiom [List_pop_get2]: forall l: ListValue, p: int, i :int:: {List_get(ListValueExcept_unwrap(List_pop(l, p)), i)}
+  (p >= 0 && p < List_len(l) && i > p) ==>
+  (List_get(ListValueExcept_unwrap(List_pop(l, p)), i) == List_get(l, i + 1));
+
+// Dict type
+type Dict := Map Value Value;
+
+//Dictionary functions
+function Dict_empty() : Dict;
+function Dict_insert (d: Dict, k: Value, v: Value) : Dict;
+function Dict_get (d: Dict, k: Value) : Value;
+function Dict_remove (d: Dict, k: Value) : Dict;
+function Dict_contains (d: Dict, k: Value) : bool {
+  Dict_get (d,k) != Value_none()
+}
+
+//Dictionary axioms
+axiom [emptydict_def]: forall k: Value :: {Dict_empty() [k]} Dict_empty() [k] == Value_none();
+axiom [Dict_get_def]: forall d: Dict, k: Value :: {Dict_get(d,k)} Dict_get(d,k) == d[normalize_value(k)];
+axiom [Dict_insert_def]: forall d: Dict, k: Value, v: Value :: {Dict_insert(d,k,v)} Dict_insert(d,k,v) == d[normalize_value(k):= v];
+axiom [Dict_remove_def]: forall d: Dict, k: Value :: {Dict_remove(d,k)} Dict_remove(d,k) == d[normalize_value(k):= Value_none()];
+
+// List of pairs of Value, used to construct Dict
+type DictList;
+// Constructor
+function DictList_nil(): DictList;
+function DictList_cons(k: Value, v: Value, d: DictList): DictList;
+//Tag and tag functions
+function DictList_tag (dl: DictList) : List_tag;
+axiom [DistListTag_nil_def]: DictList_tag (DictList_nil()) == NIL;
+axiom [DistListTag_cons_def]: forall k: Value, v: Value, d: DictList ::{DictList_cons(k,v,d)} DictList_tag (DictList_cons(k,v,d)) == CONS;
+// as a constructor for Dict
+function Dict_from_DicList (l : DictList) : Dict;
+function Dict_from_DicList_rev (l : DictList, acc: Dict) : Dict;
+axiom [Dict_from_DicList_rev_nil]: forall acc: Dict ::  Dict_from_DicList_rev(DictList_nil(), acc) == acc;
+axiom [Dict_from_DicList_rev_cons]: forall k: Value, v: Value, d: DictList, acc: Dict ::
+  Dict_from_DicList_rev(DictList_cons(k,v,d), acc) == Dict_from_DicList_rev(d,Dict_insert(acc, k, v));
+axiom [Dict_from_DicList_def]: forall dl: DictList:: {Dict_from_DicList(dl)}
+  Dict_from_DicList(dl) == Dict_from_DicList_rev(dl, Dict_empty());
+
+type ClassInstanceExcept;
+function ClassInstanceExcept_ok (ci: ClassInstance): ClassInstanceExcept;
+function ClassInstanceExcept_err (e: Error): ClassInstanceExcept;
+function ClassInstanceExcept_tag (ie: ClassInstanceExcept) : Except_tag;
+axiom [ClassInstanceExcept_tag_ok_def]: forall ci: ClassInstance :: {ClassInstanceExcept_tag(ClassInstanceExcept_ok(ci))}
+  ClassInstanceExcept_tag(ClassInstanceExcept_ok(ci)) == OK;
+axiom [ClassInstanceExcept_tag_err_def]: forall e: Error :: {ClassInstanceExcept_tag(ClassInstanceExcept_err(e))}
+  ClassInstanceExcept_tag(ClassInstanceExcept_err(e)) == ERR;
+function ClassInstanceExcept_unwrap (lie: ClassInstanceExcept) : ClassInstance;
+axiom [ClassInstanceExcept_unwrap_def]: forall ci: ClassInstance :: {ClassInstanceExcept_tag(ClassInstanceExcept_ok(ci))}
+  ClassInstanceExcept_unwrap(ClassInstanceExcept_ok(ci)) == ci;
+
+// Class type modelling
+
+function ClassInstance_mk (c: string, av: InstanceAttributes) : ClassInstance;
+
+function ClassInstance_getInstanceAttributes (ci: ClassInstance) : InstanceAttributes;
+axiom [getAttributes_def]: forall c: string, av: InstanceAttributes :: { ClassInstance_getInstanceAttributes(ClassInstance_mk (c, av))}
+  ClassInstance_getInstanceAttributes(ClassInstance_mk (c, av)) == av;
+
+function ClassInstance_getClassname (ci: ClassInstance) : string;
+axiom [get_Class_def]: forall c: string, av: InstanceAttributes :: {ClassInstance_getClassname(ClassInstance_mk (c, av))}
+  ClassInstance_getClassname(ClassInstance_mk (c, av)) == c;
+
+axiom [TypeOf_class]: forall ci: ClassInstance :: {TypeOf(Value_class(ci))} TypeOf(Value_class(ci)) == ValueType_class(ClassInstance_getClassname(ci));
+
+function InstanceAttributes_empty() : InstanceAttributes;
+axiom [AttributeValues_empty_def]: forall a: string :: {InstanceAttributes_empty()[a]}
+  InstanceAttributes_empty()[a] == ValueExcept_err(Error_AttributeError("Invalid Instance attribute of Class"));
+
+function ClassInstance_empty (c: string) : ClassInstance {
+  ClassInstance_mk(c,InstanceAttributes_empty())
+}
+
+function ClassInstance_init_InstanceAttribute(ci: ClassInstance, attribute: string, v: Value) : ClassInstance{
+  ClassInstance_mk(ClassInstance_getClassname(ci), ClassInstance_getInstanceAttributes(ci)[attribute := ValueExcept_ok(v)])
+}
+
+function ClassInstance_get_InstanceAttribute(ci: ClassInstance, attribute: string) : ValueExcept {
+  ClassInstance_getInstanceAttributes(ci)[attribute]
+}
+
+function ClassInstance_set_InstanceAttribute (ci: ClassInstance, attribute: string, value: Value): ClassInstanceExcept{
+      if ValueExcept_tag(ClassInstance_get_InstanceAttribute(ci, attribute)) == OK then
+          ClassInstanceExcept_ok(ClassInstance_mk(ClassInstance_getClassname(ci),
+                                  ClassInstance_getInstanceAttributes(ci)[attribute:=ValueExcept_ok(value)]))
+      else ClassInstanceExcept_err(Error_AttributeError("Invalid instance attribute of class"))
+}
+
+function get_ClassInstance (v: Value) : ClassInstanceExcept;
+axiom [get_ClassInstance_valid]: forall ci: ClassInstance :: {get_ClassInstance(Value_class(ci))}
+  get_ClassInstance(Value_class(ci)) == ClassInstanceExcept_ok(ci);
+axiom [get_ClassInstance_invalid]: forall v: Value :: {get_ClassInstance(v)}
+  !isClassInstance(v) ==> get_ClassInstance(v) == ClassInstanceExcept_err (Error_TypeError("Not of Class type"));
+
+function get_InstanceAttribute(v: Value, attribute: string) : ValueExcept {
+  if isClassInstance(v) then
+      ClassInstance_get_InstanceAttribute(ClassInstanceExcept_unwrap(get_ClassInstance(v)), attribute)
+  else ValueExcept_err(Error_TypeError("Not of Class type"))
+}
+
+function set_InstanceAttribute(v: Value, attribute: string, v': Value) : ValueExcept{
+  if isClassInstance(v) then
+    if (ClassInstanceExcept_tag(ClassInstance_set_InstanceAttribute(ClassInstanceExcept_unwrap(get_ClassInstance(v)), attribute, v')) == OK) then
+          ValueExcept_ok( Value_class (
+                            ClassInstanceExcept_unwrap(ClassInstance_set_InstanceAttribute(ClassInstanceExcept_unwrap(get_ClassInstance(v)), attribute, v'))
+                        ))
+    else ValueExcept_err(Error_AttributeError(("Invalid instance attribute of class")))
+  else ValueExcept_err(Error_TypeError("Not of Class type"))
+}
+
+function get_Classname (v: Value) : stringExcept {
+  if isClassInstance(v) then
+    stringExcept_ok(ClassInstance_getClassname(ClassInstanceExcept_unwrap(get_ClassInstance(v))))
+  else stringExcept_err(Error_TypeError("Not of Class type"))
+}
+
+function hasAttribute(v: Value, attribute: string): bool {
+  if isClassInstance(v) then
+    (ValueExcept_tag(ClassInstance_get_InstanceAttribute(ClassInstanceExcept_unwrap(get_ClassInstance(v)), attribute)) == OK)
+  else false
+}
+
+//Binary op functions
+function int_to_real (i: int) : real;
+function str_repeat (s: string, i: int) : string;
+function Py_add (v1: Value, v2: Value) : ValueExcept;
+function Py_sub (v1: Value, v2: Value) : ValueExcept;
+function Py_mul (v1: Value, v2: Value) : ValueExcept;
+function Py_gt (v1: Value, v2: Value) : boolExcept;
+function Py_lt (v1: Value, v2: Value) : boolExcept;
+function Py_ge (v1: Value, v2: Value) : boolExcept;
+function Py_le (v1: Value, v2: Value) : boolExcept;
+function Py_eq (v1: Value, v2: Value) : bool;
+inline function bool_to_int (b: bool) : int {if b then 1 else 0}
+inline function bool_to_real (b: bool) : real {if b then 1.0 else 0.0}
+
+axiom [Py_add_ints]: forall i1: int, i2: int :: {Py_add(Value_int(i1), Value_int(i2))}
+  Py_add(Value_int(i1), Value_int(i2)) == ValueExcept_ok(Value_int(i1 + i2));
+axiom [Py_add_floats]: forall f1: real, f2: real :: {Py_add(Value_float(f1), Value_float(f2))}
+  Py_add(Value_float(f1), Value_float(f2)) == ValueExcept_ok(Value_float(f1 + f2));
+axiom [Py_add_bools]: forall b1: bool, b2: bool :: {Py_add(Value_bool(b1), Value_bool(b2))}
+  Py_add(Value_bool(b1), Value_bool(b2)) == ValueExcept_ok(Value_int(bool_to_int(b1) + bool_to_int(b2)));
+axiom [Py_add_int_bool]: forall i: int, b: bool :: {Py_add(Value_int(i), Value_bool(b))}
+  Py_add(Value_int(i), Value_bool(b)) == ValueExcept_ok(Value_int(i + bool_to_int(b)));
+axiom [Py_add_bool_int]: forall b: bool, i: int :: {Py_add(Value_bool(b), Value_int(i))}
+  Py_add(Value_bool(b), Value_int(i)) == ValueExcept_ok(Value_int(bool_to_int(b) + i));
+axiom [Py_add_int_float]: forall i: int, r: real :: {Py_add(Value_int(i), Value_float(r))}
+  Py_add(Value_int(i), Value_float(r)) == ValueExcept_ok(Value_float(r + int_to_real(i)));
+axiom [Py_add_float_int]: forall r: real, i: int :: {Py_add(Value_float(r), Value_int(i))}
+  Py_add(Value_float(r), Value_int(i)) == ValueExcept_ok(Value_float(int_to_real(i) + r));
+axiom [Py_add_float_bool]: forall r: real, b: bool :: {Py_add(Value_float(r), Value_bool(b))}
+  Py_add(Value_float(r), Value_bool(b)) == ValueExcept_ok(Value_float(r + bool_to_real(b)));
+axiom [Py_add_bool_float]: forall b: bool, r: real :: {Py_add(Value_bool(b), Value_float(r))}
+  Py_add(Value_bool(b), Value_float(r)) == ValueExcept_ok(Value_float(bool_to_real(b) + r));
+axiom [Py_add_strs]: forall s1: string, s2: string :: {Py_add(Value_str(s1), Value_str(s2))}
+  Py_add(Value_str(s1), Value_str(s2)) == ValueExcept_ok(Value_str(str.concat(s1, s2)));
+axiom [Py_add_lists]: forall l1: ListValue, l2: ListValue :: {Py_add(Value_list(l1), Value_list(l2))}
+  Py_add(Value_list(l1), Value_list(l2)) == ValueExcept_ok(Value_list(List_extend(l1, l2)));
+axiom [Py_add_undefined]: forall v1: Value, v2: Value :: {Py_add(v1,v2)}
+  !((isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ||
+    (TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_add(v1, v2) == ValueExcept_err(Error_Undefined("Operand Type is not defined"));
+
+axiom [Py_sub_ints]: forall i1: int, i2: int :: {Py_sub(Value_int(i1), Value_int(i2))}
+  Py_sub(Value_int(i1), Value_int(i2)) == ValueExcept_ok(Value_int(i1 - i2));
+axiom [Py_sub_floats]: forall f1: real, f2: real :: {Py_sub(Value_float(f1), Value_float(f2))}
+  Py_sub(Value_float(f1), Value_float(f2)) == ValueExcept_ok(Value_float(f1 - f2));
+axiom [Py_sub_bools]: forall b1: bool, b2: bool :: {Py_sub(Value_bool(b1), Value_bool(b2))}
+  Py_sub(Value_bool(b1), Value_bool(b2)) == ValueExcept_ok(Value_int(bool_to_int(b1) - bool_to_int(b2)));
+axiom [Py_sub_int_bool]: forall i: int, b: bool :: {Py_sub(Value_int(i), Value_bool(b))}
+  Py_sub(Value_int(i), Value_bool(b)) == ValueExcept_ok(Value_int(i - bool_to_int(b)));
+axiom [Py_sub_bool_int]: forall b: bool, i: int :: {Py_sub(Value_bool(b), Value_int(i))}
+  Py_sub(Value_bool(b), Value_int(i)) == ValueExcept_ok(Value_int(bool_to_int(b) - i));
+axiom [Py_sub_int_float]: forall i: int, r: real :: {Py_sub(Value_int(i), Value_float(r))}
+  Py_sub(Value_int(i), Value_float(r)) == ValueExcept_ok(Value_float(r - int_to_real(i)));
+axiom [Py_sub_float_int]: forall r: real, i: int :: {Py_sub(Value_float(r), Value_int(i))}
+  Py_sub(Value_float(r), Value_int(i)) == ValueExcept_ok(Value_float(int_to_real(i) - r));
+axiom [Py_sub_float_bool]: forall r: real, b: bool :: {Py_sub(Value_float(r), Value_bool(b))}
+  Py_sub(Value_float(r), Value_bool(b)) == ValueExcept_ok(Value_float(r - bool_to_real(b)));
+axiom [Py_sub_bool_float]: forall b: bool, r: real :: {Py_sub(Value_bool(b), Value_float(r))}
+  Py_sub(Value_bool(b), Value_float(r)) == ValueExcept_ok(Value_float(bool_to_real(b) - r));
+axiom [Py_sub_undefined]: forall v1: Value, v2: Value :: {Py_sub(v1,v2)}
+  !(isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ==>
+  Py_sub(v1, v2) == ValueExcept_err(Error_Undefined("Operand Type is not defined"));
+
+axiom [Py_mul_ints]: forall i1: int, i2: int :: {Py_mul(Value_int(i1), Value_int(i2))}
+  Py_mul(Value_int(i1), Value_int(i2)) == ValueExcept_ok(Value_int(i1 * i2));
+axiom [Py_mul_bools]: forall b1: bool, b2: bool :: {Py_mul(Value_bool(b1), Value_bool(b2))}
+  Py_mul(Value_bool(b1), Value_bool(b2)) == ValueExcept_ok(Value_int(bool_to_int(b1) * bool_to_int(b2)));
+axiom [Py_mul_int_bool]: forall i: int, b: bool :: {Py_mul(Value_int(i), Value_bool(b))}
+  Py_mul(Value_int(i), Value_bool(b)) == ValueExcept_ok(Value_int(i * bool_to_int(b)));
+axiom [Py_mul_bool_int]: forall b: bool, i: int :: {Py_mul(Value_bool(b), Value_int(i))}
+  Py_mul(Value_bool(b), Value_int(i)) == ValueExcept_ok(Value_int(bool_to_int(b) * i));
+axiom [Py_mul_str_int]: forall s: string, i: int :: {Py_mul(Value_str(s), Value_int(i))}
+  Py_mul(Value_str(s), Value_int(i)) == ValueExcept_ok(Value_str(str_repeat(s, i)));
+axiom [Py_mul_int_str]: forall s: string, i: int :: {Py_mul(Value_int(i), Value_str(s))}
+  Py_mul(Value_int(i), Value_str(s)) == ValueExcept_ok(Value_str(str_repeat(s, i)));
+axiom [Py_mul_str_bool]: forall s: string, b: bool :: {Py_mul(Value_str(s), Value_bool(b))}
+  Py_mul(Value_str(s), Value_bool(b)) == ValueExcept_ok(Value_str(if b then s else ""));
+axiom [Py_mul_bool_str]: forall s: string, b: bool :: {Py_mul(Value_bool(b), Value_str(s)) }
+  Py_mul(Value_bool(b), Value_str(s)) ==  ValueExcept_ok(Value_str(if b then s else ""));
+axiom [Py_mul_list_int]: forall l: ListValue, i: int :: {Py_mul(Value_list(l), Value_int(i))}
+  Py_mul(Value_list(l), Value_int(i)) == ValueExcept_ok(Value_list(List_repeat(l, i)));
+axiom [Py_mul_int_list]: forall l: ListValue, i: int :: {Py_mul(Value_int(i), Value_list(l))}
+  Py_mul(Value_int(i), Value_list(l)) == ValueExcept_ok(Value_list(List_repeat(l, i)));
+axiom [Py_mul_list_bool]: forall l: ListValue, b: bool :: {Py_mul(Value_list(l), Value_bool(b))}
+  Py_mul(Value_list(l), Value_bool(b)) == ValueExcept_ok(Value_list(if b then l else ListValue_nil()));
+axiom [Py_mul_bool_list]: forall l: ListValue, b: bool :: {Py_mul(Value_bool(b), Value_list(l)) }
+  Py_mul(Value_bool(b), Value_list(l)) ==  ValueExcept_ok(Value_list(if b then l else ListValue_nil()));
+axiom [Py_mul_undefined]: forall v1: Value, v2: Value :: {Py_add(v1,v2)}
+  !((isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ||
+    (TypeOf(v1) == STR && isInstance(v2, INT)) ||
+    (TypeOf(v2) == STR && isInstance(v1, INT)) ||
+    (isList(v1) && isInstance(v2, INT)) ||
+    (isList(v2) && isInstance(v1, INT)) )
+  ==> Py_mul(v1, v2) == ValueExcept_err(Error_Undefined("Operand Type is not defined"));
+
+axiom [Py_lt_ints]: forall i1: int, i2: int :: {Py_lt(Value_int(i1), Value_int(i2))}
+  Py_lt(Value_int(i1), Value_int(i2)) == boolExcept_ok(i1 < i2);
+axiom [Py_lt_floats]: forall f1: real, f2: real :: {Py_lt(Value_float(f1), Value_float(f2))}
+  Py_lt(Value_float(f1), Value_float(f2)) == boolExcept_ok(f1 < f2);
+axiom [Py_lt_bools]: forall b1: bool, b2: bool :: {Py_lt(Value_bool(b1), Value_bool(b2))}
+  Py_lt(Value_bool(b1), Value_bool(b2)) == boolExcept_ok(bool_to_int(b1) < bool_to_int(b2));
+axiom [Py_lt_int_bool]: forall i: int, b: bool :: {Py_lt(Value_int(i), Value_bool(b))}
+  Py_lt(Value_int(i), Value_bool(b)) == boolExcept_ok(i < bool_to_int(b));
+axiom [Py_lt_bool_int]: forall b: bool, i: int :: {Py_lt(Value_bool(b), Value_int(i))}
+  Py_lt(Value_bool(b), Value_int(i)) == boolExcept_ok(bool_to_int(b) < i);
+axiom [Py_lt_int_float]: forall i: int, r: real :: {Py_lt(Value_int(i), Value_float(r))}
+  Py_lt(Value_int(i), Value_float(r)) == boolExcept_ok(r < int_to_real(i));
+axiom [Py_lt_float_int]: forall r: real, i: int :: {Py_lt(Value_float(r), Value_int(i))}
+  Py_lt(Value_float(r), Value_int(i)) == boolExcept_ok(int_to_real(i) < r);
+axiom [Py_lt_float_bool]: forall r: real, b: bool :: {Py_lt(Value_float(r), Value_bool(b))}
+  Py_lt(Value_float(r), Value_bool(b)) == boolExcept_ok(r < bool_to_real(b));
+axiom [Py_lt_bool_float]: forall b: bool, r: real :: {Py_lt(Value_bool(b), Value_float(r))}
+  Py_lt(Value_bool(b), Value_float(r)) == boolExcept_ok(bool_to_real(b) < r);
+axiom [Py_lt_undefined]: forall v1: Value, v2: Value :: {Py_lt(v1,v2)}
+  !((isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ||
+    (TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_lt(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not defined"));
+axiom [Py_lt_unsupported]: forall v1: Value, v2: Value :: {Py_lt(v1,v2)}
+  ((TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_lt(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not supported"));
+
+axiom [Py_gt_ints]: forall i1: int, i2: int :: {Py_gt(Value_int(i1), Value_int(i2))}
+  Py_gt(Value_int(i1), Value_int(i2)) == boolExcept_ok(i1 > i2);
+axiom [Py_gt_floats]: forall f1: real, f2: real :: {Py_gt(Value_float(f1), Value_float(f2))}
+  Py_gt(Value_float(f1), Value_float(f2)) == boolExcept_ok(f1 > f2);
+axiom [Py_gt_bools]: forall b1: bool, b2: bool :: {Py_gt(Value_bool(b1), Value_bool(b2))}
+  Py_gt(Value_bool(b1), Value_bool(b2)) == boolExcept_ok(bool_to_int(b1) > bool_to_int(b2));
+axiom [Py_gt_int_bool]: forall i: int, b: bool :: {Py_gt(Value_int(i), Value_bool(b))}
+  Py_gt(Value_int(i), Value_bool(b)) == boolExcept_ok(i > bool_to_int(b));
+axiom [Py_gt_bool_int]: forall b: bool, i: int :: {Py_gt(Value_bool(b), Value_int(i))}
+  Py_gt(Value_bool(b), Value_int(i)) == boolExcept_ok(bool_to_int(b) > i);
+axiom [Py_gt_int_float]: forall i: int, r: real :: {Py_gt(Value_int(i), Value_float(r))}
+  Py_gt(Value_int(i), Value_float(r)) == boolExcept_ok(r > int_to_real(i));
+axiom [Py_gt_float_int]: forall r: real, i: int :: {Py_gt(Value_float(r), Value_int(i))}
+  Py_gt(Value_float(r), Value_int(i)) == boolExcept_ok(int_to_real(i) > r);
+axiom [Py_gt_float_bool]: forall r: real, b: bool :: {Py_gt(Value_float(r), Value_bool(b))}
+  Py_gt(Value_float(r), Value_bool(b)) == boolExcept_ok(r > bool_to_real(b));
+axiom [Py_gt_bool_float]: forall b: bool, r: real :: {Py_gt(Value_bool(b), Value_float(r))}
+  Py_gt(Value_bool(b), Value_float(r)) == boolExcept_ok(bool_to_real(b) > r);
+axiom [Py_gt_undefined]: forall v1: Value, v2: Value :: {Py_gt(v1,v2)}
+  !((isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ||
+    (TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_gt(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not defined"));
+axiom [Py_gt_unsupported]: forall v1: Value, v2: Value :: {Py_gt(v1,v2)}
+  ((TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_gt(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not supported"));
+
+axiom [Py_le_ints]: forall i1: int, i2: int :: {Py_le(Value_int(i1), Value_int(i2))}
+  Py_le(Value_int(i1), Value_int(i2)) == boolExcept_ok(i1 <= i2);
+axiom [Py_le_floats]: forall f1: real, f2: real :: {Py_le(Value_float(f1), Value_float(f2))}
+  Py_le(Value_float(f1), Value_float(f2)) == boolExcept_ok(f1 <= f2);
+axiom [Py_le_bools]: forall b1: bool, b2: bool :: {Py_le(Value_bool(b1), Value_bool(b2))}
+  Py_le(Value_bool(b1), Value_bool(b2)) == boolExcept_ok(bool_to_int(b1) <= bool_to_int(b2));
+axiom [Py_le_int_bool]: forall i: int, b: bool :: {Py_le(Value_int(i), Value_bool(b))}
+  Py_le(Value_int(i), Value_bool(b)) == boolExcept_ok(i <= bool_to_int(b));
+axiom [Py_le_bool_int]: forall b: bool, i: int :: {Py_le(Value_bool(b), Value_int(i))}
+  Py_le(Value_bool(b), Value_int(i)) == boolExcept_ok(bool_to_int(b) <= i);
+axiom [Py_le_int_float]: forall i: int, r: real :: {Py_le(Value_int(i), Value_float(r))}
+  Py_le(Value_int(i), Value_float(r)) == boolExcept_ok(r <= int_to_real(i));
+axiom [Py_le_float_int]: forall r: real, i: int :: {Py_le(Value_float(r), Value_int(i))}
+  Py_le(Value_float(r), Value_int(i)) == boolExcept_ok(int_to_real(i) <= r);
+axiom [Py_le_float_bool]: forall r: real, b: bool :: {Py_le(Value_float(r), Value_bool(b))}
+  Py_le(Value_float(r), Value_bool(b)) == boolExcept_ok(r <= bool_to_real(b));
+axiom [Py_le_bool_float]: forall b: bool, r: real :: {Py_le(Value_bool(b), Value_float(r))}
+  Py_le(Value_bool(b), Value_float(r)) == boolExcept_ok(bool_to_real(b) <= r);
+axiom [Py_le_undefined]: forall v1: Value, v2: Value :: {Py_le(v1,v2)}
+  !((isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ||
+    (TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_le(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not defined"));
+axiom [Py_le_unsupported]: forall v1: Value, v2: Value :: {Py_le(v1,v2)}
+  ((TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_le(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not supported"));
+
+axiom [Py_ge_ints]: forall i1: int, i2: int :: {Py_ge(Value_int(i1), Value_int(i2))}
+  Py_ge(Value_int(i1), Value_int(i2)) == boolExcept_ok(i1 >= i2);
+axiom [Py_ge_floats]: forall f1: real, f2: real :: {Py_ge(Value_float(f1), Value_float(f2))}
+  Py_ge(Value_float(f1), Value_float(f2)) == boolExcept_ok(f1 >= f2);
+axiom [Py_ge_bools]: forall b1: bool, b2: bool :: {Py_ge(Value_bool(b1), Value_bool(b2))}
+  Py_ge(Value_bool(b1), Value_bool(b2)) == boolExcept_ok(bool_to_int(b1) >= bool_to_int(b2));
+axiom [Py_ge_int_bool]: forall i: int, b: bool :: {Py_ge(Value_int(i), Value_bool(b))}
+  Py_ge(Value_int(i), Value_bool(b)) == boolExcept_ok(i >= bool_to_int(b));
+axiom [Py_ge_bool_int]: forall b: bool, i: int :: {Py_ge(Value_bool(b), Value_int(i))}
+  Py_ge(Value_bool(b), Value_int(i)) == boolExcept_ok(bool_to_int(b) >= i);
+axiom [Py_ge_int_float]: forall i: int, r: real :: {Py_ge(Value_int(i), Value_float(r))}
+  Py_ge(Value_int(i), Value_float(r)) == boolExcept_ok(r >= int_to_real(i));
+axiom [Py_ge_float_int]: forall r: real, i: int :: {Py_ge(Value_float(r), Value_int(i))}
+  Py_ge(Value_float(r), Value_int(i)) == boolExcept_ok(int_to_real(i) >= r);
+axiom [Py_ge_float_bool]: forall r: real, b: bool :: {Py_ge(Value_float(r), Value_bool(b))}
+  Py_ge(Value_float(r), Value_bool(b)) == boolExcept_ok(r >= bool_to_real(b));
+axiom [Py_ge_bool_float]: forall b: bool, r: real :: {Py_ge(Value_bool(b), Value_float(r))}
+  Py_ge(Value_bool(b), Value_float(r)) == boolExcept_ok(bool_to_real(b) >= r);
+axiom [Py_ge_undefined]: forall v1: Value, v2: Value :: {Py_ge(v1,v2)}
+  !((isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ||
+    (TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_ge(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not defined"));
+axiom [Py_ge_unsupported]: forall v1: Value, v2: Value :: {Py_ge(v1,v2)}
+  ((TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_ge(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not supported"));
+
+function Py_add_unwrap (v1: Value, v2: Value) : Value {
+  ValueExcept_unwrap (Py_add (v1,v2))
+}
+function Py_sub_unwrap (v1: Value, v2: Value) : Value {
+  ValueExcept_unwrap (Py_sub (v1,v2))
+}
+function Py_mul_unwrap (v1: Value, v2: Value) : Value {
+  ValueExcept_unwrap (Py_mul (v1,v2))
+}
+function Py_gt_unwrap (v1: Value, v2: Value) : bool {
+  boolExcept_unwrap (Py_gt (v1,v2))
+}
+function Py_lt_unwrap (v1: Value, v2: Value) : bool {
+  boolExcept_unwrap (Py_lt (v1,v2))
+}
+function Py_ge_unwrap (v1: Value, v2: Value) : bool {
+  boolExcept_unwrap (Py_ge (v1,v2))
+}
+function Py_le_unwrap (v1: Value, v2: Value) : bool {
+  boolExcept_unwrap (Py_le (v1,v2))
+}
+
+
+axiom [Py_eq_def]: forall v: Value, v': Value :: {Py_eq(v, v')}
+  Py_eq(v, v') == (normalize_value(v) == normalize_value (v'));
+
+type ExceptOrNone;
+type DictStrAny;
+
+#end
+
+--#eval verify "cvc5" boogieTypePrelude
+--#eval boogieTypePrelude.format
+
+def Boogie.Typeprelude : Boogie.Program :=
+   Boogie.getProgram Strata.boogieTypePrelude |>.fst
+
+end Strata
diff --git a/Strata/Languages/Python/BoogieTypePreludeTest.lean b/Strata/Languages/Python/BoogieTypePreludeTest.lean
new file mode 100644
index 000000000..a5c875a55
--- /dev/null
+++ b/Strata/Languages/Python/BoogieTypePreludeTest.lean
@@ -0,0 +1,922 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DDM.Elab
+import Strata.DDM.AST
+import Strata.Languages.Boogie.DDMTransform.Parse
+import Strata.Languages.Boogie.Verifier
+
+namespace Strata
+
+def boogieTypePrelude :=
+#strata
+program Boogie;
+
+//Generic tag for List
+type List_tag;
+const CONS : List_tag;
+const NIL : List_tag;
+axiom [list_tag_unique]: CONS != NIL;
+axiom [all_list_tag]: forall lt: List_tag :: lt == CONS || lt == NIL;
+
+type Error;
+
+// Constructors
+function Error_TypeError (msg : string) : Error;
+function Error_AttributeError (msg : string) : Error;
+function Error_RePatternError (msg : string) : Error;
+function Error_Unimplemented (msg : string) : Error;
+function Error_Undefined (msg : string) : Error;
+
+type Error_tag;
+const TYPEERR : Error_tag;
+const ATRERR : Error_tag;
+const REERR : Error_tag;
+const UNIMPLERR : Error_tag;
+const UNDEFERR : Error_tag;
+axiom [error_tag_unique]: TYPEERR != ATRERR && TYPEERR != REERR && TYPEERR != UNIMPLERR && TYPEERR != UNDEFERR &&
+                          ATRERR != REERR && ATRERR != UNIMPLERR && ATRERR != UNDEFERR &&
+                          REERR != UNIMPLERR && REERR != UNDEFERR &&
+                          UNIMPLERR != UNDEFERR ;
+
+axiom [all_error_tag]: forall et: Error_tag :: et == TYPEERR || et == ATRERR || et == REERR || et == UNIMPLERR || et == UNDEFERR;
+
+function ErrorTag (e: Error) : Error_tag;
+axiom [ErrorTag_def_typeerr]: forall msg: string :: {ErrorTag(Error_TypeError(msg))} ErrorTag(Error_TypeError(msg)) == TYPEERR;
+axiom [ErrorTag_def_attrerr]: forall msg: string :: {ErrorTag(Error_AttributeError(msg))} ErrorTag(Error_AttributeError(msg)) == ATRERR;
+axiom [ErrorTag_def_reerr]: forall msg: string :: {ErrorTag(Error_RePatternError(msg))} ErrorTag(Error_RePatternError(msg)) == REERR;
+axiom [ErrorTag_def_unimplerr]: forall msg: string :: {ErrorTag(Error_Unimplemented(msg))} ErrorTag(Error_Unimplemented(msg)) == UNIMPLERR;
+axiom [ErrorTag_def_undeferr]: forall msg: string :: {ErrorTag(Error_Undefined(msg))} ErrorTag(Error_Undefined(msg)) == UNDEFERR;
+
+type Except_tag;
+const OK : Except_tag;
+const ERR : Except_tag;
+axiom [except_tag_unique]: OK != ERR;
+axiom [all_except_tag]: forall et: Except_tag :: et == OK || et == ERR;
+
+type stringExcept;
+function stringExcept_ok (s: string): stringExcept;
+function stringExcept_err (e: Error): stringExcept;
+function stringExcept_tag (ie: stringExcept) : Except_tag;
+axiom [stringExcept_tag_ok_def]: forall s: string :: {stringExcept_tag(stringExcept_ok(s))}
+  stringExcept_tag(stringExcept_ok(s)) == OK;
+axiom [stringExcept_tag_err_def]: forall e: Error :: {stringExcept_tag(stringExcept_err(e))}
+  stringExcept_tag(stringExcept_err(e)) == ERR;
+function stringExcept_unwrap (lie: stringExcept) : string;
+axiom [stringExcept_unwrap_def]: forall s: string :: {stringExcept_tag(stringExcept_ok(s))}
+  stringExcept_unwrap(stringExcept_ok(s)) == s;
+
+type boolExcept;
+function boolExcept_ok (b: bool): boolExcept;
+function boolExcept_err (e: Error): boolExcept;
+function boolExcept_tag (be: boolExcept) : Except_tag;
+axiom [boolExcept_tag_ok_def]: forall b: bool :: {boolExcept_tag(boolExcept_ok(b))}
+  boolExcept_tag(boolExcept_ok(b)) == OK;
+axiom [boolExcept_tag_err_def]: forall e: Error :: {boolExcept_tag(boolExcept_err(e))}
+  boolExcept_tag(boolExcept_err(e)) == ERR;
+function boolExcept_unwrap (lie: boolExcept) : bool;
+axiom [boolExcept_unwrap_def]: forall b: bool :: {boolExcept_tag(boolExcept_ok(b))}
+  boolExcept_unwrap(boolExcept_ok(b)) == b;
+
+type intExcept;
+function intExcept_ok (i: int): intExcept;
+function intExcept_err (e: Error): intExcept;
+function intExcept_tag (ie: intExcept) : Except_tag;
+axiom [intExcept_tag_ok_def]: forall i: int :: {intExcept_tag(intExcept_ok(i))}
+  intExcept_tag(intExcept_ok(i)) == OK;
+axiom [intExcept_tag_err_def]: forall e: Error :: {intExcept_tag(intExcept_err(e))}
+  intExcept_tag(intExcept_err(e)) == ERR;
+function intExcept_unwrap (lie: intExcept) : int;
+axiom [intExcept_unwrap_def]: forall i: int :: {intExcept_tag(intExcept_ok(i))}
+  intExcept_unwrap(intExcept_ok(i)) == i;
+
+type Datetime;
+
+// Value and ListValue types
+type Value;
+type ListValue;
+
+type ValueExcept;
+function ValueExcept_ok (v: Value): ValueExcept;
+function ValueExcept_err (e: Error): ValueExcept;
+function ValueExcept_tag (ve: ValueExcept) : Except_tag;
+axiom [ValueExcept_tag_ok_def]: forall v: Value :: {ValueExcept_tag(ValueExcept_ok(v))}
+  ValueExcept_tag(ValueExcept_ok(v)) == OK;
+axiom [ValueExcept_tag_err_def]: forall e: Error :: {ValueExcept_tag(ValueExcept_err(e))}
+  ValueExcept_tag(ValueExcept_err(e)) == ERR;
+function ValueExcept_unwrap (lve: ValueExcept) : Value;
+axiom [ValueExcept_unwrap_def]: forall v: Value :: {ValueExcept_tag(ValueExcept_ok(v))}
+  ValueExcept_unwrap(ValueExcept_ok(v)) == v;
+
+// Class type
+type InstanceAttributes := Map string ValueExcept;
+type ClassInstance;
+
+// Constructors
+function Value_bool (b : bool) : Value;
+function Value_int (i : int) : Value;
+function Value_float (f : real) : Value;
+function Value_str (s : string) : Value;
+function Value_datetime (d : Datetime) : Value;
+function Value_none() : Value;
+function Value_list (lv : ListValue) : Value;
+function Value_class (ci: ClassInstance) : Value;
+
+function ListValue_nil() : ListValue;
+function ListValue_cons(x0 : Value, x1 : ListValue) : ListValue;
+//Tags
+function ListValue_tag (l: ListValue) : List_tag;
+axiom [ListValue_tag_nil_def]: ListValue_tag (ListValue_nil()) == NIL;
+axiom [ListValue_tag_cons_def]: forall v: Value, vs: ListValue ::{ListValue_cons(v, vs)} ListValue_tag (ListValue_cons(v, vs)) == CONS;
+
+// Types of Value
+type ValueType;
+type ListValueType;
+const BOOL : ValueType;
+const INT : ValueType;
+const FLOAT : ValueType;
+const STR : ValueType;
+const DATETIME : ValueType;
+const NONE : ValueType;
+function ValueType_class(classname: string): ValueType;
+
+function isListValueType (t: ValueType): bool;
+function isClassValueType (t: ValueType): bool;
+axiom [isClassType_def]: forall c: string :: {isClassValueType(ValueType_class(c))} isClassValueType(ValueType_class(c));
+
+//Uniqueness axioms
+axiom [unique_ValueType_DATETIME]: DATETIME != BOOL && DATETIME != INT && DATETIME != FLOAT && DATETIME != STR && DATETIME != NONE && !isListValueType(DATETIME) && !(isClassValueType(DATETIME));
+axiom [unique_ValueType_bool]: BOOL != INT && BOOL != FLOAT && BOOL != STR && BOOL != NONE && !isListValueType(BOOL) && !(isClassValueType(BOOL));
+axiom [unique_ValueType_int]: INT != STR && INT != FLOAT && INT != NONE && !isListValueType(INT) && !(isClassValueType(INT));
+axiom [unique_ValueType_float]: FLOAT != STR && FLOAT != NONE && !isListValueType(FLOAT) && !(isClassValueType(FLOAT));
+axiom [unique_ValueType_str]: STR != NONE && !isListValueType(STR) && !(isClassValueType(STR));
+axiom [unique_ValueType_none]: !isListValueType(NONE) && !(isClassValueType(NONE));
+axiom [classtype_ne_listtype]: forall t: ValueType :: {isListValueType (t), isClassValueType (t)} !(isListValueType (t) && isClassValueType (t));
+axiom [all_ValueType_cases]: forall t: ValueType ::
+  t == BOOL ||
+  t == INT ||
+  t == FLOAT ||
+  t == STR ||
+  t == NONE ||
+  t == DATETIME ||
+  isListValueType (t) ||
+  isClassValueType (t);
+
+//Eq axioms
+axiom [value_int_eq]: forall i: int, j: int :: {Value_int(i) == Value_int(j)} (Value_int(i) == Value_int(j)) == (i == j);
+axiom [value_bool_eq]: forall b1: bool, b2: bool :: {Value_bool(b1) == Value_bool(b2)} (Value_bool(b1) == Value_bool(b2)) == (b1 == b2);
+axiom [value_float_eq]: forall r1: real, r2: real :: {Value_float(r1) == Value_float(r2)} (Value_float(r1) == Value_float(r2)) == (r1 == r2);
+axiom [value_str_eq]: forall s1: string, s2: string :: {Value_str(s1) == Value_str(s2)} (Value_str(s1) == Value_str(s2)) == (s1 == s2);
+axiom [value_datetime_eq]: forall d1: Datetime, d2: Datetime :: {Value_datetime(d1) == Value_datetime(d2)} (Value_datetime(d1) == Value_datetime(d2)) == (d1 == d2);
+
+//Constructors and tag functions of ListType
+function ListType_nil() : (ListValueType);
+function ListType_cons(x0 : ValueType, x1 : ListValueType) : ListValueType;
+function ValueType_List (l: ListValueType) : ValueType;
+function ListValueType_tag (l: ListValueType) : List_tag;
+axiom [ListValueType_tag_nil_def]: ListValueType_tag (ListType_nil()) == NIL;
+axiom [ListValueType_tag_cons_def]: forall t: ValueType, ts: ListValueType ::{ListType_cons(t, ts)} (ListValueType_tag (ListType_cons(t, ts)) == CONS);
+axiom [isListValueType_def]: forall l: ListValueType ::{isListValueType(ValueType_List (l))} isListValueType(ValueType_List (l));
+
+// TypeOf and TypesOf functions
+function TypeOf (v : Value) : ValueType;
+function TypesOf (v: ListValue) : ListValueType;
+// Definitions
+axiom [TypesOf_nil_def]: TypesOf(ListValue_nil()) == ListType_nil();
+axiom [TypesOf_cons_def]: forall v: Value, vs: ListValue ::{ListValue_cons(v, vs)} TypesOf(ListValue_cons(v, vs)) == ListType_cons(TypeOf(v), TypesOf(vs));
+axiom [TypeOf_list_def]: forall l: ListValue ::{Value_list(l)} TypeOf(Value_list(l)) ==  ValueType_List(TypesOf(l));
+axiom [TypeOf_bool]: forall b: bool :: {TypeOf(Value_bool(b))} TypeOf(Value_bool(b)) == BOOL;
+axiom [TypeOf_int]: forall i: int :: {Value_int(i)} TypeOf(Value_int(i)) == INT;
+axiom [TypeOf_float]: forall f: real :: {Value_float(f)} TypeOf(Value_float(f)) == FLOAT;
+axiom [TypeOf_str]: forall s: string :: {Value_str(s)} TypeOf(Value_str(s)) == STR;
+axiom [TypeOf_datetime]: forall d: Datetime :: {Value_datetime(d)} TypeOf(Value_datetime(d)) == DATETIME;
+axiom [TypeOf_none]: TypeOf(Value_none()) == NONE;
+axiom [TypeOf_list]: forall l: ListValue :: {Value_list(l)} TypeOf(Value_list(l)) == ValueType_List(TypesOf(l));
+
+axiom [TypeOf_bool_exists]: forall v: Value :: {TypeOf(v) == BOOL} TypeOf(v) == BOOL ==> exists b: bool :: v == Value_bool(b);
+axiom [TypeOf_int_exists]: forall v: Value :: {TypeOf(v) == INT} TypeOf(v) == INT ==> exists i: int :: v == Value_int(i);
+axiom [TypeOf_float_exists]: forall v: Value :: {TypeOf(v) == FLOAT} TypeOf(v) == FLOAT ==> exists r: real :: v == Value_float(r);
+axiom [TypeOf_string_exists]: forall v: Value :: {TypeOf(v) == STR} TypeOf(v) == STR ==> exists s: string :: v == Value_str(s);
+axiom [TypeOf_none']: forall v: Value :: {TypeOf(v) == NONE} (TypeOf(v) == NONE) == (v == Value_none()) ;
+
+function isBool (v: Value): bool {
+  TypeOf(v) == BOOL
+}
+function isInt (v: Value): bool {
+  TypeOf(v) == INT
+}
+function isStr (v: Value): bool {
+  TypeOf(v) == STR
+}
+function isFloat (v: Value): bool{
+  TypeOf(v) == FLOAT
+}
+function isNone (v: Value): bool{
+  TypeOf(v) == NONE
+}
+function isDatetime (v: Value): bool{
+  TypeOf(v) == DATETIME
+}
+
+function isList (v: Value): bool;
+function isClassInstance (v: Value): bool;
+
+axiom [isList_def]: forall l: ListValue :: {Value_list(l)} isList(Value_list(l));
+axiom [isList_def']: forall v: Value :: {isListValueType(TypeOf(v))} isList(v) == isListValueType(TypeOf(v));
+axiom [isClassInstance_def]: forall ci: ClassInstance :: {Value_class(ci)} isClassInstance(Value_class(ci));
+axiom [isClassInstance_def']: forall v: Value :: {isClassValueType(TypeOf(v))} isClassInstance(v) == isClassValueType(TypeOf(v));
+
+axiom [TypeOf_list_exists]: forall v: Value :: {isList(v)} isList(v) ==> exists l: ListValue :: v == Value_list(l);
+axiom [TypeOf_class_exists]: forall v: Value :: {isClassInstance(v)} isClassInstance(v) ==> exists ci: ClassInstance :: v == Value_class(ci);
+
+
+//Casting
+function as_bool (v: Value) : bool;
+axiom [as_bool_def]: forall b: bool :: {as_bool(Value_bool(b))} as_bool(Value_bool(b)) == b;
+
+// isSubType functions
+function isSubType (t1: ValueType, t2: ValueType) : bool;
+function isSubTypes (t1: ListValueType, t2: ListValueType) : bool;
+//Definitions
+axiom [isSubTypes_nil_def]: isSubTypes(ListType_nil(), ListType_nil());
+axiom [not_isSubTypes_nil]: forall ty: ValueType, l: ListValueType :: !isSubTypes(ListType_nil(), ListType_cons(ty,l));
+axiom [not_isSubTypes_nil']: forall ty: ValueType, l: ListValueType :: !isSubTypes(ListType_cons(ty,l), ListType_nil());
+axiom [isSubTypes_cons_def]:forall t: ValueType, ts: ListValueType, t': ValueType, ts': ListValueType  ::{ListType_cons(t, ts), ListType_cons(t', ts')}
+  isSubTypes(ListType_cons(t, ts), ListType_cons(t', ts')) == (isSubType(t, t') && isSubTypes(ts, ts'));
+axiom [isSubType_list_def]: forall l: ListValueType, l': ListValueType :: {ValueType_List(l), ValueType_List(l')}
+  isSubType(ValueType_List(l), ValueType_List(l')) == isSubTypes(l, l');
+axiom [bool_substype_int]: isSubType(BOOL, INT);
+axiom [int_substype_float]: isSubType(INT, FLOAT);
+axiom [not_isSubstype_string]: forall t: ValueType ::{isSubType(STR, t), isSubType(t,STR)}
+  t == STR || (!isSubType(STR, t) && !isSubType(t,STR));
+axiom [not_isSubstype_none]: forall t: ValueType ::{isSubType(NONE, t), isSubType(NONE, t)}
+  t == NONE || (!isSubType(NONE, t) && !isSubType(t,NONE));
+axiom [not_isSubstype_list]: forall t: ValueType, t': ValueType ::{isSubType(t, t')}
+  ((isListValueType(t) && !isListValueType(t')) || (!isListValueType(t) && isListValueType(t'))) ==> (!isSubType(t, t') && !isSubType(t', t));
+axiom [not_isSubstype_class_othertypes]: forall t: ValueType, t': ValueType ::{isSubType(t, t')}
+  ((isClassValueType(t) && !isClassValueType(t')) || (!isClassValueType(t) && isClassValueType(t'))) ==> (!isSubType(t, t') && !isSubType(t', t));
+axiom [not_isSubstype_class]: forall t: ValueType, c: string ::{isSubType(ValueType_class(c), t), isSubType(t,ValueType_class(c))}
+  t != ValueType_class(c) ==> (!isSubType(ValueType_class(c), t) && !isSubType(t,ValueType_class(c)));
+// Supporting lemmas
+axiom [isSubtype_rfl]: forall t: ValueType::{isSubType (t,t)} isSubType (t,t);
+axiom [isSubtype_mono]: forall t1: ValueType, t2: ValueType ::{isSubType (t1,t2)} !isSubType (t1,t2) || (t1 == t2 || !isSubType(t2,t1));
+axiom [isSubtype_trans]: forall t1: ValueType, t2: ValueType, t3: ValueType::{isSubType(t1, t2)} !(isSubType(t1, t2) && isSubType(t2, t3)) || isSubType(t1, t3);
+
+// isInstance function:
+function isInstance (v: Value, vt: ValueType) : bool;
+axiom [isInstance_of_isSubtype]: forall v: Value, t: ValueType::{isInstance(v,t)} isInstance(v,t) == isSubType(TypeOf(v), t);
+
+function is_IntReal (v: Value) : bool;
+function Value_real_to_int (v: Value) : int;
+// to be extended
+function normalize_value (v : Value) : Value {
+  if v == Value_bool(true) then Value_int(1)
+  else (if v == Value_bool(false) then Value_int(0) else
+        if TypeOf(v) == FLOAT && is_IntReal(v) then Value_int(Value_real_to_int(v)) else
+        v)
+}
+
+type ListValueExcept;
+function ListValueExcept_ok (l: ListValue): ListValueExcept;
+function ListValueExcept_err (e: Error): ListValueExcept;
+function ListValueExcept_tag (lve: ListValueExcept) : Except_tag;
+axiom [ListValueExcept_tag_ok_def]: forall l: ListValue :: {ListValueExcept_tag(ListValueExcept_ok(l))}
+  ListValueExcept_tag(ListValueExcept_ok(l)) == OK;
+axiom [ListValueExcept_tag_err_def]: forall e: Error :: {ListValueExcept_tag(ListValueExcept_err(e))}
+  ListValueExcept_tag(ListValueExcept_err(e)) == ERR;
+function ListValueExcept_unwrap (lve: ListValueExcept) : ListValue;
+axiom [ListValueExcept_unwrap_def]: forall l: ListValue :: {ListValueExcept_tag(ListValueExcept_ok(l))}
+  ListValueExcept_unwrap(ListValueExcept_ok(l)) == l;
+
+// ListValue functions
+function List_contains (l : ListValue, x: Value) : bool;
+function List_len (l : ListValue) : int;
+function List_extend (l1 : ListValue, l2: ListValue) : ListValue;
+function List_append (l: ListValue, x: Value) : ListValue;
+function List_get (l : ListValue, i : int) : ValueExcept;
+function List_reverse (l: ListValue) : ListValue;
+function List_index! (l: ListValue, v: Value): int;
+function List_index (l: ListValue, v: Value): intExcept;
+function List_repeat (l: ListValue, n: int): ListValue;
+function List_insert (l: ListValue, i: int, v: Value): ListValue;
+function List_remove (l: ListValue, v: Value): ListValue;
+//TO BE done
+function List_pop (l: ListValue, i: int): ListValueExcept;
+
+//List function axioms
+axiom [List_contains_nil_def]: forall x : Value ::{List_contains(ListValue_nil(), x)}
+  !List_contains(ListValue_nil(), x);
+axiom [List_contains_cons_def]: forall x : Value, h : Value, t : ListValue ::{List_contains(ListValue_cons(h,t),x)}
+  List_contains(ListValue_cons(h,t),x) == ((normalize_value(x)==normalize_value(h)) || List_contains(t, x));
+
+axiom [List_len_nil_def]: List_len (ListValue_nil()) == 0;
+axiom [List_len_cons_def]: forall h : Value, t : ListValue ::{List_len (ListValue_cons(h,t))}
+  List_len (ListValue_cons(h,t)) == 1 + List_len(t);
+axiom [List_len_nonneg]: forall l: ListValue :: {List_len(l)} List_len(l) >= 0 ;
+axiom [List_nil_of_len_zero]: forall l: ListValue :: {List_len(l) == 0}
+  (List_len(l) == 0) == (l == ListValue_nil());
+
+axiom [List_extend_nil_def]: forall l1: ListValue ::{List_extend (l1, ListValue_nil())}
+  List_extend (l1, ListValue_nil()) == l1;
+axiom [List_nil_extend_def]: forall l1: ListValue ::{List_extend (ListValue_nil(), l1)}
+  List_extend (ListValue_nil(), l1) == l1;
+axiom [List_cons_extend_def]: forall h: Value, t: ListValue, l2: ListValue  ::{List_extend (ListValue_cons(h,t), l2)}
+  List_extend (ListValue_cons(h,t), l2) == ListValue_cons(h, List_extend(t,l2));
+
+axiom [List_cons_extend_contains]: forall x: Value, l1: ListValue, l2: ListValue  ::{List_contains (List_extend(l1,l2), x)}
+  List_contains (List_extend(l1,l2), x) == (List_contains (l1,x) || List_contains(l2,x));
+axiom [List_len_extend]: forall l1: ListValue, l2: ListValue  ::{List_len (List_extend(l1,l2))}
+  List_len (List_extend(l1,l2)) == List_len (l1) + List_len(l2);
+axiom [List_extend_assoc]: forall l1: ListValue, l2: ListValue, l3: ListValue :: {List_extend(List_extend(l1,l2), l3)}
+  List_extend(List_extend(l1,l2), l3) == List_extend(l1,List_extend(l2,l3));
+
+axiom [List_get_nil]: forall i : int ::{List_get (ListValue_nil(), i)}
+  List_get (ListValue_nil(), i) == ValueExcept_err(Error_Undefined("index out of bound"));
+axiom [List_get_zero]: forall h : Value, t : ListValue ::{List_get (ListValue_cons(h,t), 0)}
+  List_get (ListValue_cons(h,t), 0) == ValueExcept_ok(h);
+axiom [List_get_ind]: forall h : Value, t : ListValue, i : int ::{List_get (ListValue_cons(h,t), i)}
+  (i > 0) ==> (List_get (ListValue_cons(h,t), i)) == List_get (t, i - 1);
+axiom [List_get_contains]: forall l: ListValue, i: int, x: Value :: {List_contains(l,x), List_get(l,i)}
+  (List_get(l,i) == ValueExcept_ok(x)) ==> List_contains(l,x);
+axiom [List_get_contains_eq]: forall l: ListValue, x: Value :: {List_contains(l,x)}
+  List_contains(l,x) == (exists i:int :: {} List_get(l,i) == ValueExcept_ok(x));
+axiom [List_get_ok]: forall l: ListValue, i: int:: {List_get(l,i)}
+  ((List_get(l,i)) != ValueExcept_err(Error_Undefined("index out of bound"))) == (i < List_len(l) && i >= 0);
+axiom [List_get_ok']: forall l: ListValue, i: int:: {List_get(l,i)}
+  (ValueExcept_tag(List_get(l,i)) != ERR) == (i < List_len(l) && i >= 0);
+axiom [List_extend_get]: forall l1: ListValue, l2: ListValue, i: int :: {List_get(List_extend(l1,l2), i)}
+  List_get(List_extend(l1,l2), i) == if i < List_len(l1) then List_get(l1, i) else List_get(l2, i - List_len(l1));
+
+axiom [List_append_def]: forall l: ListValue, x: Value :: {List_append(l,x)}
+  List_append(l,x) == List_extend(l, ListValue_cons(x, ListValue_nil()));
+
+axiom [List_reverse_def_nil]: List_reverse(ListValue_nil()) == ListValue_nil();
+axiom [List_reverse_def_cons]: forall h: Value, t: ListValue:: {List_reverse(ListValue_cons(h,t))}
+  List_reverse(ListValue_cons(h,t)) == List_append(List_reverse(t), h);
+axiom [List_reverse_len]: forall l: ListValue :: {List_len(List_reverse(l))}
+  List_len(l) == List_len(List_reverse(l));
+axiom [List_reverse_contain]: forall l: ListValue, v: Value :: {List_contains (List_reverse(l), v)}
+  List_contains (List_reverse(l), v) == List_contains(l,v);
+axiom [List_reverse_index]: forall l: ListValue, i: int :: {List_get(List_reverse(l), i)}
+  List_get(List_reverse(l), i) == List_get(l, List_len(l)-1-i);
+axiom [List_reverse_reverse]: forall l: ListValue :: {List_reverse(List_reverse(l))}
+  List_reverse(List_reverse(l)) == l;
+axiom [List_reverse_extend]: forall l1: ListValue, l2: ListValue :: {List_reverse(List_extend(l1,l2))}
+  List_reverse(List_extend(l1,l2)) == List_extend(List_reverse(l2), List_reverse(l1));
+
+axiom [List_index!_nil_def]: forall v: Value :: {List_index!(ListValue_nil(), v)}
+  List_index!(ListValue_nil(), v) == 0;
+axiom [List_index!_cons_def_1]: forall h: Value, t: ListValue :: {List_index!(ListValue_cons(h,t), h)}
+  List_index!(ListValue_cons(h,t), h) == 0;
+axiom [List_index!_cons_def_2]: forall v: Value, h: Value, t: ListValue :: {List_index!(ListValue_cons(h,t), v)}
+  !(normalize_value(v)==normalize_value(h)) ==> List_index!(ListValue_cons(h,t), v) == List_index!(t, v) + 1;
+axiom [List_index_def]: forall v: Value, l: ListValue :: {List_index(l, v)}
+  List_index(l,v) ==  if (List_index!(l,v) == List_len(l)) then intExcept_err(Error_Undefined("List does not contain element"))
+                      else intExcept_ok(List_index!(l,v));
+
+axiom [List_repeat_def]: forall l: ListValue, n: int :: {List_repeat(l, n)}
+  List_repeat(l, n) ==  if (n <= 0) then ListValue_nil() else
+                        if (n == 1) then l else  List_extend(l, List_repeat(l, n-1));
+axiom [List_repeat_mul]: forall l: ListValue, n: int, m: int :: {List_repeat(List_repeat(l, n),m)}
+  List_repeat(List_repeat(l, n),m) == List_repeat(l, n * m);
+axiom [List_repeat_len]: forall l: ListValue, n: int :: {List_len(List_repeat(l, n))}
+  n > 0 ==> List_len(List_repeat(l, n)) == n * List_len(l);
+axiom [List_repeat_contain]: forall l: ListValue, v: Value, n: int :: {List_contains(List_repeat(l, n), v)}
+  n > 0 ==> (List_contains(List_repeat(l, n), v) == List_contains(l, v));
+axiom [List_repeat_get]: forall l: ListValue, v: Value, i: int, n: int, m: int :: {List_get(List_repeat(l, n), i + m * List_len(l))}
+  (i >= 0 && i < List_len(l) && m >= 0 && m < n) ==> (List_get(List_repeat(l, n), i + m * List_len(l)) == List_get(l, i));
+
+axiom [List_insert_def0]: forall i: int, v: Value :: {List_insert(ListValue_nil(), i, v)}
+  List_insert(ListValue_nil(), i, v) == ListValue_cons(v, ListValue_nil());
+axiom [List_insert_def1]: forall l: ListValue, i: int, v: Value :: {List_insert(l, i, v)}
+  i <= 0 ==> List_insert(l, i, v) == ListValue_cons(v, l);
+axiom [List_insert_def2]: forall h: Value, t: ListValue, i: int, v: Value :: {List_insert(ListValue_cons(h,t), i, v)}
+  (i > 0) ==> List_insert(ListValue_cons(h,t), i, v) == ListValue_cons(h, List_insert(t, i-1, v));
+axiom [List_insert_len]: forall l: ListValue, i: int, v: Value :: {List_len(List_insert(l, i, v))}
+  List_len(List_insert(l, i, v)) == List_len(l) + 1;
+axiom [List_insert_get0]: forall l: ListValue, p: int, v: Value:: {List_get(List_insert(l, p, v), p)}
+  (p >= 0 && p < List_len(l)) ==> (List_get(List_insert(l, p, v), p) == ValueExcept_ok(v));
+axiom [List_insert_get1]: forall l: ListValue, p: int, v: Value:: {List_get(List_insert(l, p, v), p)}
+  p >= List_len(l) ==> (List_get(List_insert(l, p, v), List_len(l)) == ValueExcept_ok(v));
+axiom [List_insert_get2]: forall l: ListValue, p: int, v: Value, i: int :: {List_get(List_insert(l, p, v), i)}
+  (p >= List_len(l) && i < List_len(l)) ==> (List_get(List_insert(l, p, v),i) == List_get(l, i));
+axiom [List_insert_get3]: forall l: ListValue, p: int, v: Value, i: int:: {List_get(List_insert(l, p, v), i)}
+  (p >= 0 && p < List_len(l) && i < p) ==> (List_get(List_insert(l, p, v), i) == List_get(l,i));
+axiom [List_insert_get4]: forall l: ListValue, p: int, v: Value, i: int:: {List_get(List_insert(l, p, v), i)}
+  (p >= 0 && p < List_len(l) && i > p) ==> (List_get(List_insert(l, p, v), i) == List_get(l,i -1));
+axiom [List_insert_get6]: forall l: ListValue, p: int, v: Value, i: int:: {List_get(List_insert(l, p, v), i)}
+  (p <= 0 && i > 0) ==> (List_get(List_insert(l, p, v), i) == List_get(l,i -1));
+axiom [List_insert_contains]: forall l: ListValue, i: int, v: Value :: {List_contains(List_insert(l,i,v),v)}
+  List_contains(List_insert(l,i,v),v);
+
+axiom [List_remove_nil_def]: forall x : Value ::{List_remove(ListValue_nil(), x)}
+  List_remove(ListValue_nil(), x) == ListValue_nil();
+axiom [List_remove_cons_def]: forall x : Value, h : Value, t : ListValue ::{List_remove(ListValue_cons(h,t),x)}
+  List_remove(ListValue_cons(h,t),x) == if (normalize_value(x)==normalize_value(h)) then t
+                                        else ListValue_cons(h, List_remove(t, x));
+axiom [List_remove_len]: forall l: ListValue, x: Value :: {List_len(List_remove(l,x))}
+  List_len(List_remove(l,x)) == if (List_contains(l,x)) then (List_len(l) - 1) else List_len(l);
+axiom [List_remove_not_contain]: forall l: ListValue, x: Value :: {List_remove(l,x)}
+  (!List_contains(l,x)) == (List_remove(l,x) == l);
+
+axiom [List_pop_def0]: forall i: int :: {List_pop(ListValue_nil(), i)}
+  List_pop(ListValue_nil(), i) == ListValueExcept_err(Error_Undefined("Pop from empty list"));
+axiom [List_pop_def1]: forall h: Value, t: ListValue:: {List_pop(ListValue_cons(h,t), 0)}
+  List_pop(ListValue_cons(h,t), 0) == ListValueExcept_ok(t);
+axiom [List_pop_def2]: forall h: Value, t: ListValue, i: int :: {List_pop(ListValue_cons(h,t), i)}
+   List_pop(ListValue_cons(h,t), i) ==
+    if (i > 0 && i <= List_len(t)) then
+        ListValueExcept_ok(ListValue_cons(h, ListValueExcept_unwrap(List_pop(t, i-1))))
+    else ListValueExcept_err(Error_Undefined("Pop outside of index range"));
+axiom [List_pop_def3]: forall h: Value, t: ListValue, i: int :: {List_pop(ListValue_cons(h,t), i)}
+  (i < 0) ==> List_pop(ListValue_cons(h,t), i) == ListValueExcept_err(Error_Undefined("Pop outside of index range"));
+axiom [List_pop_len]: forall l: ListValue, i: int :: {List_len(ListValueExcept_unwrap(List_pop(l, i)))}
+  List_len(ListValueExcept_unwrap(List_pop(l, i))) == List_len(l) - 1;
+axiom [List_pop_get0]: forall l: ListValue, p: int, i :int:: {List_get(ListValueExcept_unwrap(List_pop(l, p)), i)}
+  (p >= 0 && p < List_len(l) && i < p) ==>
+  (List_get(ListValueExcept_unwrap(List_pop(l, p)), i) == List_get(l, i));
+axiom [List_pop_get2]: forall l: ListValue, p: int, i :int:: {List_get(ListValueExcept_unwrap(List_pop(l, p)), i)}
+  (p >= 0 && p < List_len(l) && i > p) ==>
+  (List_get(ListValueExcept_unwrap(List_pop(l, p)), i) == List_get(l, i + 1));
+
+// Dict type
+type Dict := Map Value Value;
+
+//Dictionary functions
+function Dict_empty() : Dict;
+function Dict_insert (d: Dict, k: Value, v: Value) : Dict;
+function Dict_get (d: Dict, k: Value) : Value;
+function Dict_remove (d: Dict, k: Value) : Dict;
+function Dict_contains (d: Dict, k: Value) : bool {
+  Dict_get (d,k) != Value_none()
+}
+
+//Dictionary axioms
+axiom [emptydict_def]: forall k: Value :: {Dict_empty() [k]} Dict_empty() [k] == Value_none();
+axiom [Dict_get_def]: forall d: Dict, k: Value :: {Dict_get(d,k)} Dict_get(d,k) == d[normalize_value(k)];
+axiom [Dict_insert_def]: forall d: Dict, k: Value, v: Value :: {Dict_insert(d,k,v)} Dict_insert(d,k,v) == d[normalize_value(k):= v];
+axiom [Dict_remove_def]: forall d: Dict, k: Value :: {Dict_remove(d,k)} Dict_remove(d,k) == d[normalize_value(k):= Value_none()];
+
+// List of pairs of Value, used to construct Dict
+type DictList;
+// Constructor
+function DictList_nil(): DictList;
+function DictList_cons(k: Value, v: Value, d: DictList): DictList;
+//Tag and tag functions
+function DictList_tag (dl: DictList) : List_tag;
+axiom [DistListTag_nil_def]: DictList_tag (DictList_nil()) == NIL;
+axiom [DistListTag_cons_def]: forall k: Value, v: Value, d: DictList ::{DictList_cons(k,v,d)} DictList_tag (DictList_cons(k,v,d)) == CONS;
+// as a constructor for Dict
+function Dict_from_DicList (l : DictList) : Dict;
+function Dict_from_DicList_rev (l : DictList, acc: Dict) : Dict;
+axiom [Dict_from_DicList_rev_nil]: forall acc: Dict ::  Dict_from_DicList_rev(DictList_nil(), acc) == acc;
+axiom [Dict_from_DicList_rev_cons]: forall k: Value, v: Value, d: DictList, acc: Dict ::
+  Dict_from_DicList_rev(DictList_cons(k,v,d), acc) == Dict_from_DicList_rev(d,Dict_insert(acc, k, v));
+axiom [Dict_from_DicList_def]: forall dl: DictList:: {Dict_from_DicList(dl)}
+  Dict_from_DicList(dl) == Dict_from_DicList_rev(dl, Dict_empty());
+
+type ClassInstanceExcept;
+function ClassInstanceExcept_ok (ci: ClassInstance): ClassInstanceExcept;
+function ClassInstanceExcept_err (e: Error): ClassInstanceExcept;
+function ClassInstanceExcept_tag (ie: ClassInstanceExcept) : Except_tag;
+axiom [ClassInstanceExcept_tag_ok_def]: forall ci: ClassInstance :: {ClassInstanceExcept_tag(ClassInstanceExcept_ok(ci))}
+  ClassInstanceExcept_tag(ClassInstanceExcept_ok(ci)) == OK;
+axiom [ClassInstanceExcept_tag_err_def]: forall e: Error :: {ClassInstanceExcept_tag(ClassInstanceExcept_err(e))}
+  ClassInstanceExcept_tag(ClassInstanceExcept_err(e)) == ERR;
+function ClassInstanceExcept_unwrap (lie: ClassInstanceExcept) : ClassInstance;
+axiom [ClassInstanceExcept_unwrap_def]: forall ci: ClassInstance :: {ClassInstanceExcept_tag(ClassInstanceExcept_ok(ci))}
+  ClassInstanceExcept_unwrap(ClassInstanceExcept_ok(ci)) == ci;
+
+// Class type modelling
+
+function ClassInstance_mk (c: string, av: InstanceAttributes) : ClassInstance;
+
+function ClassInstance_getInstanceAttributes (ci: ClassInstance) : InstanceAttributes;
+axiom [getAttributes_def]: forall c: string, av: InstanceAttributes :: { ClassInstance_getInstanceAttributes(ClassInstance_mk (c, av))}
+  ClassInstance_getInstanceAttributes(ClassInstance_mk (c, av)) == av;
+
+function ClassInstance_getClassname (ci: ClassInstance) : string;
+axiom [get_Class_def]: forall c: string, av: InstanceAttributes :: {ClassInstance_getClassname(ClassInstance_mk (c, av))}
+  ClassInstance_getClassname(ClassInstance_mk (c, av)) == c;
+
+axiom [TypeOf_class]: forall ci: ClassInstance :: {TypeOf(Value_class(ci))} TypeOf(Value_class(ci)) == ValueType_class(ClassInstance_getClassname(ci));
+
+function InstanceAttributes_empty() : InstanceAttributes;
+axiom [AttributeValues_empty_def]: forall a: string :: {InstanceAttributes_empty()[a]}
+  InstanceAttributes_empty()[a] == ValueExcept_err(Error_AttributeError("Invalid Instance attribute of Class"));
+
+function ClassInstance_empty (c: string) : ClassInstance {
+  ClassInstance_mk(c,InstanceAttributes_empty())
+}
+
+function ClassInstance_init_InstanceAttribute(ci: ClassInstance, attribute: string, v: Value) : ClassInstance{
+  ClassInstance_mk(ClassInstance_getClassname(ci), ClassInstance_getInstanceAttributes(ci)[attribute := ValueExcept_ok(v)])
+}
+
+function ClassInstance_get_InstanceAttribute(ci: ClassInstance, attribute: string) : ValueExcept {
+  ClassInstance_getInstanceAttributes(ci)[attribute]
+}
+
+function ClassInstance_set_InstanceAttribute (ci: ClassInstance, attribute: string, value: Value): ClassInstanceExcept{
+      if ValueExcept_tag(ClassInstance_get_InstanceAttribute(ci, attribute)) == OK then
+          ClassInstanceExcept_ok(ClassInstance_mk(ClassInstance_getClassname(ci),
+                                  ClassInstance_getInstanceAttributes(ci)[attribute:=ValueExcept_ok(value)]))
+      else ClassInstanceExcept_err(Error_AttributeError("Invalid instance attribute of class"))
+}
+
+function get_ClassInstance (v: Value) : ClassInstanceExcept;
+axiom [get_ClassInstance_valid]: forall ci: ClassInstance :: {get_ClassInstance(Value_class(ci))}
+  get_ClassInstance(Value_class(ci)) == ClassInstanceExcept_ok(ci);
+axiom [get_ClassInstance_invalid]: forall v: Value :: {get_ClassInstance(v)}
+  !isClassInstance(v) ==> get_ClassInstance(v) == ClassInstanceExcept_err (Error_TypeError("Not of Class type"));
+
+function get_InstanceAttribute(v: Value, attribute: string) : ValueExcept {
+  if isClassInstance(v) then
+      ClassInstance_get_InstanceAttribute(ClassInstanceExcept_unwrap(get_ClassInstance(v)), attribute)
+  else ValueExcept_err(Error_TypeError("Not of Class type"))
+}
+
+function set_InstanceAttribute(v: Value, attribute: string, v': Value) : ValueExcept{
+  if isClassInstance(v) then
+    if (ClassInstanceExcept_tag(ClassInstance_set_InstanceAttribute(ClassInstanceExcept_unwrap(get_ClassInstance(v)), attribute, v')) == OK) then
+          ValueExcept_ok( Value_class (
+                            ClassInstanceExcept_unwrap(ClassInstance_set_InstanceAttribute(ClassInstanceExcept_unwrap(get_ClassInstance(v)), attribute, v'))
+                        ))
+    else ValueExcept_err(Error_AttributeError(("Invalid instance attribute of class")))
+  else ValueExcept_err(Error_TypeError("Not of Class type"))
+}
+
+function get_Classname (v: Value) : stringExcept {
+  if isClassInstance(v) then
+    stringExcept_ok(ClassInstance_getClassname(ClassInstanceExcept_unwrap(get_ClassInstance(v))))
+  else stringExcept_err(Error_TypeError("Not of Class type"))
+}
+
+function hasAttribute(v: Value, attribute: string): bool {
+  if isClassInstance(v) then
+    (ValueExcept_tag(ClassInstance_get_InstanceAttribute(ClassInstanceExcept_unwrap(get_ClassInstance(v)), attribute)) == OK)
+  else false
+}
+
+//Binary op functions
+function int_to_real (i: int) : real;
+function str_repeat (s: string, i: int) : string;
+function Py_add (v1: Value, v2: Value) : ValueExcept;
+function Py_sub (v1: Value, v2: Value) : ValueExcept;
+function Py_mul (v1: Value, v2: Value) : ValueExcept;
+function Py_gt (v1: Value, v2: Value) : boolExcept;
+function Py_lt (v1: Value, v2: Value) : boolExcept;
+function Py_ge (v1: Value, v2: Value) : boolExcept;
+function Py_le (v1: Value, v2: Value) : boolExcept;
+function Py_eq (v1: Value, v2: Value) : bool;
+inline function bool_to_int (b: bool) : int {if b then 1 else 0}
+inline function bool_to_real (b: bool) : real {if b then 1.0 else 0.0}
+
+axiom [Py_add_ints]: forall i1: int, i2: int :: {Py_add(Value_int(i1), Value_int(i2))}
+  Py_add(Value_int(i1), Value_int(i2)) == ValueExcept_ok(Value_int(i1 + i2));
+axiom [Py_add_floats]: forall f1: real, f2: real :: {Py_add(Value_float(f1), Value_float(f2))}
+  Py_add(Value_float(f1), Value_float(f2)) == ValueExcept_ok(Value_float(f1 + f2));
+axiom [Py_add_bools]: forall b1: bool, b2: bool :: {Py_add(Value_bool(b1), Value_bool(b2))}
+  Py_add(Value_bool(b1), Value_bool(b2)) == ValueExcept_ok(Value_int(bool_to_int(b1) + bool_to_int(b2)));
+axiom [Py_add_int_bool]: forall i: int, b: bool :: {Py_add(Value_int(i), Value_bool(b))}
+  Py_add(Value_int(i), Value_bool(b)) == ValueExcept_ok(Value_int(i + bool_to_int(b)));
+axiom [Py_add_bool_int]: forall b: bool, i: int :: {Py_add(Value_bool(b), Value_int(i))}
+  Py_add(Value_bool(b), Value_int(i)) == ValueExcept_ok(Value_int(bool_to_int(b) + i));
+axiom [Py_add_int_float]: forall i: int, r: real :: {Py_add(Value_int(i), Value_float(r))}
+  Py_add(Value_int(i), Value_float(r)) == ValueExcept_ok(Value_float(r + int_to_real(i)));
+axiom [Py_add_float_int]: forall r: real, i: int :: {Py_add(Value_float(r), Value_int(i))}
+  Py_add(Value_float(r), Value_int(i)) == ValueExcept_ok(Value_float(int_to_real(i) + r));
+axiom [Py_add_float_bool]: forall r: real, b: bool :: {Py_add(Value_float(r), Value_bool(b))}
+  Py_add(Value_float(r), Value_bool(b)) == ValueExcept_ok(Value_float(r + bool_to_real(b)));
+axiom [Py_add_bool_float]: forall b: bool, r: real :: {Py_add(Value_bool(b), Value_float(r))}
+  Py_add(Value_bool(b), Value_float(r)) == ValueExcept_ok(Value_float(bool_to_real(b) + r));
+axiom [Py_add_strs]: forall s1: string, s2: string :: {Py_add(Value_str(s1), Value_str(s2))}
+  Py_add(Value_str(s1), Value_str(s2)) == ValueExcept_ok(Value_str(str.concat(s1, s2)));
+axiom [Py_add_lists]: forall l1: ListValue, l2: ListValue :: {Py_add(Value_list(l1), Value_list(l2))}
+  Py_add(Value_list(l1), Value_list(l2)) == ValueExcept_ok(Value_list(List_extend(l1, l2)));
+axiom [Py_add_undefined]: forall v1: Value, v2: Value :: {Py_add(v1,v2)}
+  !((isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ||
+    (TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_add(v1, v2) == ValueExcept_err(Error_Undefined("Operand Type is not defined"));
+
+axiom [Py_sub_ints]: forall i1: int, i2: int :: {Py_sub(Value_int(i1), Value_int(i2))}
+  Py_sub(Value_int(i1), Value_int(i2)) == ValueExcept_ok(Value_int(i1 - i2));
+axiom [Py_sub_floats]: forall f1: real, f2: real :: {Py_sub(Value_float(f1), Value_float(f2))}
+  Py_sub(Value_float(f1), Value_float(f2)) == ValueExcept_ok(Value_float(f1 - f2));
+axiom [Py_sub_bools]: forall b1: bool, b2: bool :: {Py_sub(Value_bool(b1), Value_bool(b2))}
+  Py_sub(Value_bool(b1), Value_bool(b2)) == ValueExcept_ok(Value_int(bool_to_int(b1) - bool_to_int(b2)));
+axiom [Py_sub_int_bool]: forall i: int, b: bool :: {Py_sub(Value_int(i), Value_bool(b))}
+  Py_sub(Value_int(i), Value_bool(b)) == ValueExcept_ok(Value_int(i - bool_to_int(b)));
+axiom [Py_sub_bool_int]: forall b: bool, i: int :: {Py_sub(Value_bool(b), Value_int(i))}
+  Py_sub(Value_bool(b), Value_int(i)) == ValueExcept_ok(Value_int(bool_to_int(b) - i));
+axiom [Py_sub_int_float]: forall i: int, r: real :: {Py_sub(Value_int(i), Value_float(r))}
+  Py_sub(Value_int(i), Value_float(r)) == ValueExcept_ok(Value_float(r - int_to_real(i)));
+axiom [Py_sub_float_int]: forall r: real, i: int :: {Py_sub(Value_float(r), Value_int(i))}
+  Py_sub(Value_float(r), Value_int(i)) == ValueExcept_ok(Value_float(int_to_real(i) - r));
+axiom [Py_sub_float_bool]: forall r: real, b: bool :: {Py_sub(Value_float(r), Value_bool(b))}
+  Py_sub(Value_float(r), Value_bool(b)) == ValueExcept_ok(Value_float(r - bool_to_real(b)));
+axiom [Py_sub_bool_float]: forall b: bool, r: real :: {Py_sub(Value_bool(b), Value_float(r))}
+  Py_sub(Value_bool(b), Value_float(r)) == ValueExcept_ok(Value_float(bool_to_real(b) - r));
+axiom [Py_sub_undefined]: forall v1: Value, v2: Value :: {Py_sub(v1,v2)}
+  !(isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ==>
+  Py_sub(v1, v2) == ValueExcept_err(Error_Undefined("Operand Type is not defined"));
+
+axiom [Py_mul_ints]: forall i1: int, i2: int :: {Py_mul(Value_int(i1), Value_int(i2))}
+  Py_mul(Value_int(i1), Value_int(i2)) == ValueExcept_ok(Value_int(i1 * i2));
+axiom [Py_mul_bools]: forall b1: bool, b2: bool :: {Py_mul(Value_bool(b1), Value_bool(b2))}
+  Py_mul(Value_bool(b1), Value_bool(b2)) == ValueExcept_ok(Value_int(bool_to_int(b1) * bool_to_int(b2)));
+axiom [Py_mul_int_bool]: forall i: int, b: bool :: {Py_mul(Value_int(i), Value_bool(b))}
+  Py_mul(Value_int(i), Value_bool(b)) == ValueExcept_ok(Value_int(i * bool_to_int(b)));
+axiom [Py_mul_bool_int]: forall b: bool, i: int :: {Py_mul(Value_bool(b), Value_int(i))}
+  Py_mul(Value_bool(b), Value_int(i)) == ValueExcept_ok(Value_int(bool_to_int(b) * i));
+axiom [Py_mul_str_int]: forall s: string, i: int :: {Py_mul(Value_str(s), Value_int(i))}
+  Py_mul(Value_str(s), Value_int(i)) == ValueExcept_ok(Value_str(str_repeat(s, i)));
+axiom [Py_mul_int_str]: forall s: string, i: int :: {Py_mul(Value_int(i), Value_str(s))}
+  Py_mul(Value_int(i), Value_str(s)) == ValueExcept_ok(Value_str(str_repeat(s, i)));
+axiom [Py_mul_str_bool]: forall s: string, b: bool :: {Py_mul(Value_str(s), Value_bool(b))}
+  Py_mul(Value_str(s), Value_bool(b)) == ValueExcept_ok(Value_str(if b then s else ""));
+axiom [Py_mul_bool_str]: forall s: string, b: bool :: {Py_mul(Value_bool(b), Value_str(s)) }
+  Py_mul(Value_bool(b), Value_str(s)) ==  ValueExcept_ok(Value_str(if b then s else ""));
+axiom [Py_mul_list_int]: forall l: ListValue, i: int :: {Py_mul(Value_list(l), Value_int(i))}
+  Py_mul(Value_list(l), Value_int(i)) == ValueExcept_ok(Value_list(List_repeat(l, i)));
+axiom [Py_mul_int_list]: forall l: ListValue, i: int :: {Py_mul(Value_int(i), Value_list(l))}
+  Py_mul(Value_int(i), Value_list(l)) == ValueExcept_ok(Value_list(List_repeat(l, i)));
+axiom [Py_mul_list_bool]: forall l: ListValue, b: bool :: {Py_mul(Value_list(l), Value_bool(b))}
+  Py_mul(Value_list(l), Value_bool(b)) == ValueExcept_ok(Value_list(if b then l else ListValue_nil()));
+axiom [Py_mul_bool_list]: forall l: ListValue, b: bool :: {Py_mul(Value_bool(b), Value_list(l)) }
+  Py_mul(Value_bool(b), Value_list(l)) ==  ValueExcept_ok(Value_list(if b then l else ListValue_nil()));
+axiom [Py_mul_undefined]: forall v1: Value, v2: Value :: {Py_add(v1,v2)}
+  !((isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ||
+    (TypeOf(v1) == STR && isInstance(v2, INT)) ||
+    (TypeOf(v2) == STR && isInstance(v1, INT)) ||
+    (isList(v1) && isInstance(v2, INT)) ||
+    (isList(v2) && isInstance(v1, INT)) )
+  ==> Py_mul(v1, v2) == ValueExcept_err(Error_Undefined("Operand Type is not defined"));
+
+axiom [Py_lt_ints]: forall i1: int, i2: int :: {Py_lt(Value_int(i1), Value_int(i2))}
+  Py_lt(Value_int(i1), Value_int(i2)) == boolExcept_ok(i1 < i2);
+axiom [Py_lt_floats]: forall f1: real, f2: real :: {Py_lt(Value_float(f1), Value_float(f2))}
+  Py_lt(Value_float(f1), Value_float(f2)) == boolExcept_ok(f1 < f2);
+axiom [Py_lt_bools]: forall b1: bool, b2: bool :: {Py_lt(Value_bool(b1), Value_bool(b2))}
+  Py_lt(Value_bool(b1), Value_bool(b2)) == boolExcept_ok(bool_to_int(b1) < bool_to_int(b2));
+axiom [Py_lt_int_bool]: forall i: int, b: bool :: {Py_lt(Value_int(i), Value_bool(b))}
+  Py_lt(Value_int(i), Value_bool(b)) == boolExcept_ok(i < bool_to_int(b));
+axiom [Py_lt_bool_int]: forall b: bool, i: int :: {Py_lt(Value_bool(b), Value_int(i))}
+  Py_lt(Value_bool(b), Value_int(i)) == boolExcept_ok(bool_to_int(b) < i);
+axiom [Py_lt_int_float]: forall i: int, r: real :: {Py_lt(Value_int(i), Value_float(r))}
+  Py_lt(Value_int(i), Value_float(r)) == boolExcept_ok(r < int_to_real(i));
+axiom [Py_lt_float_int]: forall r: real, i: int :: {Py_lt(Value_float(r), Value_int(i))}
+  Py_lt(Value_float(r), Value_int(i)) == boolExcept_ok(int_to_real(i) < r);
+axiom [Py_lt_float_bool]: forall r: real, b: bool :: {Py_lt(Value_float(r), Value_bool(b))}
+  Py_lt(Value_float(r), Value_bool(b)) == boolExcept_ok(r < bool_to_real(b));
+axiom [Py_lt_bool_float]: forall b: bool, r: real :: {Py_lt(Value_bool(b), Value_float(r))}
+  Py_lt(Value_bool(b), Value_float(r)) == boolExcept_ok(bool_to_real(b) < r);
+axiom [Py_lt_undefined]: forall v1: Value, v2: Value :: {Py_lt(v1,v2)}
+  !((isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ||
+    (TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_lt(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not defined"));
+axiom [Py_lt_unsupported]: forall v1: Value, v2: Value :: {Py_lt(v1,v2)}
+  ((TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_lt(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not supported"));
+
+axiom [Py_gt_ints]: forall i1: int, i2: int :: {Py_gt(Value_int(i1), Value_int(i2))}
+  Py_gt(Value_int(i1), Value_int(i2)) == boolExcept_ok(i1 > i2);
+axiom [Py_gt_floats]: forall f1: real, f2: real :: {Py_gt(Value_float(f1), Value_float(f2))}
+  Py_gt(Value_float(f1), Value_float(f2)) == boolExcept_ok(f1 > f2);
+axiom [Py_gt_bools]: forall b1: bool, b2: bool :: {Py_gt(Value_bool(b1), Value_bool(b2))}
+  Py_gt(Value_bool(b1), Value_bool(b2)) == boolExcept_ok(bool_to_int(b1) > bool_to_int(b2));
+axiom [Py_gt_int_bool]: forall i: int, b: bool :: {Py_gt(Value_int(i), Value_bool(b))}
+  Py_gt(Value_int(i), Value_bool(b)) == boolExcept_ok(i > bool_to_int(b));
+axiom [Py_gt_bool_int]: forall b: bool, i: int :: {Py_gt(Value_bool(b), Value_int(i))}
+  Py_gt(Value_bool(b), Value_int(i)) == boolExcept_ok(bool_to_int(b) > i);
+axiom [Py_gt_int_float]: forall i: int, r: real :: {Py_gt(Value_int(i), Value_float(r))}
+  Py_gt(Value_int(i), Value_float(r)) == boolExcept_ok(r > int_to_real(i));
+axiom [Py_gt_float_int]: forall r: real, i: int :: {Py_gt(Value_float(r), Value_int(i))}
+  Py_gt(Value_float(r), Value_int(i)) == boolExcept_ok(int_to_real(i) > r);
+axiom [Py_gt_float_bool]: forall r: real, b: bool :: {Py_gt(Value_float(r), Value_bool(b))}
+  Py_gt(Value_float(r), Value_bool(b)) == boolExcept_ok(r > bool_to_real(b));
+axiom [Py_gt_bool_float]: forall b: bool, r: real :: {Py_gt(Value_bool(b), Value_float(r))}
+  Py_gt(Value_bool(b), Value_float(r)) == boolExcept_ok(bool_to_real(b) > r);
+axiom [Py_gt_undefined]: forall v1: Value, v2: Value :: {Py_gt(v1,v2)}
+  !((isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ||
+    (TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_gt(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not defined"));
+axiom [Py_gt_unsupported]: forall v1: Value, v2: Value :: {Py_gt(v1,v2)}
+  ((TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_gt(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not supported"));
+
+axiom [Py_le_ints]: forall i1: int, i2: int :: {Py_le(Value_int(i1), Value_int(i2))}
+  Py_le(Value_int(i1), Value_int(i2)) == boolExcept_ok(i1 <= i2);
+axiom [Py_le_floats]: forall f1: real, f2: real :: {Py_le(Value_float(f1), Value_float(f2))}
+  Py_le(Value_float(f1), Value_float(f2)) == boolExcept_ok(f1 <= f2);
+axiom [Py_le_bools]: forall b1: bool, b2: bool :: {Py_le(Value_bool(b1), Value_bool(b2))}
+  Py_le(Value_bool(b1), Value_bool(b2)) == boolExcept_ok(bool_to_int(b1) <= bool_to_int(b2));
+axiom [Py_le_int_bool]: forall i: int, b: bool :: {Py_le(Value_int(i), Value_bool(b))}
+  Py_le(Value_int(i), Value_bool(b)) == boolExcept_ok(i <= bool_to_int(b));
+axiom [Py_le_bool_int]: forall b: bool, i: int :: {Py_le(Value_bool(b), Value_int(i))}
+  Py_le(Value_bool(b), Value_int(i)) == boolExcept_ok(bool_to_int(b) <= i);
+axiom [Py_le_int_float]: forall i: int, r: real :: {Py_le(Value_int(i), Value_float(r))}
+  Py_le(Value_int(i), Value_float(r)) == boolExcept_ok(r <= int_to_real(i));
+axiom [Py_le_float_int]: forall r: real, i: int :: {Py_le(Value_float(r), Value_int(i))}
+  Py_le(Value_float(r), Value_int(i)) == boolExcept_ok(int_to_real(i) <= r);
+axiom [Py_le_float_bool]: forall r: real, b: bool :: {Py_le(Value_float(r), Value_bool(b))}
+  Py_le(Value_float(r), Value_bool(b)) == boolExcept_ok(r <= bool_to_real(b));
+axiom [Py_le_bool_float]: forall b: bool, r: real :: {Py_le(Value_bool(b), Value_float(r))}
+  Py_le(Value_bool(b), Value_float(r)) == boolExcept_ok(bool_to_real(b) <= r);
+axiom [Py_le_undefined]: forall v1: Value, v2: Value :: {Py_le(v1,v2)}
+  !((isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ||
+    (TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_le(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not defined"));
+axiom [Py_le_unsupported]: forall v1: Value, v2: Value :: {Py_le(v1,v2)}
+  ((TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_le(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not supported"));
+
+axiom [Py_ge_ints]: forall i1: int, i2: int :: {Py_ge(Value_int(i1), Value_int(i2))}
+  Py_ge(Value_int(i1), Value_int(i2)) == boolExcept_ok(i1 >= i2);
+axiom [Py_ge_floats]: forall f1: real, f2: real :: {Py_ge(Value_float(f1), Value_float(f2))}
+  Py_ge(Value_float(f1), Value_float(f2)) == boolExcept_ok(f1 >= f2);
+axiom [Py_ge_bools]: forall b1: bool, b2: bool :: {Py_ge(Value_bool(b1), Value_bool(b2))}
+  Py_ge(Value_bool(b1), Value_bool(b2)) == boolExcept_ok(bool_to_int(b1) >= bool_to_int(b2));
+axiom [Py_ge_int_bool]: forall i: int, b: bool :: {Py_ge(Value_int(i), Value_bool(b))}
+  Py_ge(Value_int(i), Value_bool(b)) == boolExcept_ok(i >= bool_to_int(b));
+axiom [Py_ge_bool_int]: forall b: bool, i: int :: {Py_ge(Value_bool(b), Value_int(i))}
+  Py_ge(Value_bool(b), Value_int(i)) == boolExcept_ok(bool_to_int(b) >= i);
+axiom [Py_ge_int_float]: forall i: int, r: real :: {Py_ge(Value_int(i), Value_float(r))}
+  Py_ge(Value_int(i), Value_float(r)) == boolExcept_ok(r >= int_to_real(i));
+axiom [Py_ge_float_int]: forall r: real, i: int :: {Py_ge(Value_float(r), Value_int(i))}
+  Py_ge(Value_float(r), Value_int(i)) == boolExcept_ok(int_to_real(i) >= r);
+axiom [Py_ge_float_bool]: forall r: real, b: bool :: {Py_ge(Value_float(r), Value_bool(b))}
+  Py_ge(Value_float(r), Value_bool(b)) == boolExcept_ok(r >= bool_to_real(b));
+axiom [Py_ge_bool_float]: forall b: bool, r: real :: {Py_ge(Value_bool(b), Value_float(r))}
+  Py_ge(Value_bool(b), Value_float(r)) == boolExcept_ok(bool_to_real(b) >= r);
+axiom [Py_ge_undefined]: forall v1: Value, v2: Value :: {Py_ge(v1,v2)}
+  !((isInstance(v1, FLOAT) && isInstance(v2, FLOAT)) ||
+    (TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_ge(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not defined"));
+axiom [Py_ge_unsupported]: forall v1: Value, v2: Value :: {Py_ge(v1,v2)}
+  ((TypeOf(v1) == STR && TypeOf(v2) == STR) ||
+    (isList(v1) && isList(v2)))
+  ==> Py_ge(v1, v2) == boolExcept_err(Error_Undefined("Operand Type is not supported"));
+
+axiom [Py_eq_def]: forall v: Value, v': Value :: {Py_eq(v, v')}
+  Py_eq(v, v') == (normalize_value(v) == normalize_value (v'));
+
+function Py_add_unwrap (v1: Value, v2: Value) : Value {
+  ValueExcept_unwrap (Py_add (v1,v2))
+}
+function Py_sub_unwrap (v1: Value, v2: Value) : Value {
+  ValueExcept_unwrap (Py_sub (v1,v2))
+}
+function Py_mul_unwrap (v1: Value, v2: Value) : Value {
+  ValueExcept_unwrap (Py_mul (v1,v2))
+}
+function Py_gt_unwrap (v1: Value, v2: Value) : bool {
+  boolExcept_unwrap (Py_gt (v1,v2))
+}
+function Py_lt_unwrap (v1: Value, v2: Value) : bool {
+  boolExcept_unwrap (Py_lt (v1,v2))
+}
+function Py_ge_unwrap (v1: Value, v2: Value) : bool {
+  boolExcept_unwrap (Py_ge (v1,v2))
+}
+function Py_le_unwrap (v1: Value, v2: Value) : bool {
+  boolExcept_unwrap (Py_le (v1,v2))
+}
+
+
+//Testing
+procedure non_contradiction_test() returns () {
+  assert [one_eq_two_expect_unknown]: 1 == 2;
+};
+
+procedure binary_op_and_types_test () returns () {
+  assert [int_add_ok]: forall i: int :: ValueExcept_tag(Py_add(Value_int(1), Value_int(i))) != ERR;
+  assert [int_add_class_except]: forall v: Value :: isClassInstance(v) ==> ValueExcept_tag(Py_add(Value_int(1), v)) == ERR;
+  assert [int_add_class_except']: forall v: Value :: hasAttribute(v, "a") ==> ValueExcept_tag(Py_add(Value_int(1), v)) == ERR;
+  assert [float_add_isInstance_int_ok]: forall v: Value :: isInstance(v,INT) ==> ValueExcept_tag(Py_add(Value_float(1.1), v)) != ERR;
+};
+
+procedure ValueTypeTest() returns () {
+  var ty1: ValueType, ty2: ValueType, tl: ValueType;
+  ty1 := TypeOf(Value_int(5));
+  ty2 := TypeOf(Value_bool(true));
+  assert [subtype1]: isSubType(ty2,ty1);
+  assert [subtypeList]: forall l: ListValueType :: isSubType (ValueType_List(ListType_cons(ty2, l)), ValueType_List(ListType_cons(ty1, l)));
+  assert [subtypeList2]: forall l1: ListValueType, l2: ListValueType :: !(isSubTypes(l1,l2)) || isSubType (ValueType_List(ListType_cons(ty2, l1)), ValueType_List(ListType_cons(ty1, l2)));
+};
+
+procedure simple_call(v1: Value, v2: Value) returns ()
+  spec {
+    requires [v1_type]: isInstance(v1, BOOL) || isInstance(v1, STR);
+    requires [v2_type]: isInstance(v2, ValueType_List(ListType_cons(INT, ListType_cons(INT, ListType_nil()))));
+  }
+{};
+
+procedure test_simple_call_argument_typecheck() returns () {
+  var arg1: Value, arg2: Value;
+  arg1 := Value_bool(true);
+  arg2 := Value_list(ListValue_cons(Value_int(3), ListValue_cons (Value_bool(true), ListValue_nil())));
+  assert [subtype_bool]: isInstance(arg1,BOOL);
+  call simple_call(arg1, arg2);
+};
+
+procedure list_functions_test() returns ()
+{
+  var l1: ListValue, l2: ListValue;
+  l1 := ListValue_cons(Value_int(1), ListValue_cons(Value_int(2), ListValue_cons (Value_int(3), ListValue_nil())));
+  l2 := ListValue_cons(Value_int(1), ListValue_cons(Value_int(2), ListValue_cons (Value_int(3),
+        ListValue_cons(Value_int(1), ListValue_cons(Value_int(2), ListValue_cons (Value_int(3), ListValue_nil()))))));
+  assert [index_1]: List_get(l1,1) == ValueExcept_ok(Value_int(2));
+  assert [contain_true]: List_contains(l1, Value_bool(true));
+  assert [ValueEq]: !(Value_int(4) == Value_int(3));
+  assert [normalize_value]: !(normalize_value(Value_int(4)) == Value_int(3));
+  assert [contain_3]: List_contains(l1, Value_int(2));
+  assert [list_index_test1]: List_index(l1, Value_int(3)) == intExcept_ok(2);
+  assert [list_index_test_expect_unknown]: List_index(l1, Value_int(3)) == intExcept_ok(3);
+  assert [list_index_test2]: intExcept_tag(List_index(l1, Value_int(9))) == ERR;
+  assert [list_extend]: List_extend(l1, l1) == l2;
+  assert [list_repeat1]: List_repeat(l1, 2) == l2;
+  assert [list_repeat2]: List_repeat(l1, 6) == List_repeat(l2, 3);
+};
+
+procedure list_generic_test() returns () {
+  var l1: ListValue;
+  assert [contains_append]: forall l: ListValue, x: Value :: List_contains(List_append(l,x), x);
+  assert [len_append]: forall l: ListValue, x: Value :: List_len(List_append(l,x)) == List_len(l) + 1;
+  l1 := ListValue_cons(Value_int(1), ListValue_cons(Value_int(2), ListValue_cons (Value_int(3), ListValue_nil())));
+  assert [l1_contains_3]: List_contains (l1, Value_int(3));
+  assert [contains_len]: forall l: ListValue, x: Value:: List_contains(l,x) ==> (List_len(l) >0);
+  assert [l1l2_contains_3]: forall l2: ListValue :: List_contains (List_extend(l1, l2), Value_int(3));
+  assert [revl1_contain_3]: List_contains (List_reverse(l1), Value_int(3));
+  assert [rev_contain]: forall l: ListValue, v: Value :: List_contains (List_reverse(l), v) == List_contains(l,v);
+  assert [l1r_l2_contains_3]: forall l2: ListValue :: List_contains (List_extend(List_reverse(l1), l2), Value_int(3));
+  assert [l1r_l2_contains_4_expect_unknown]: forall l2: ListValue :: List_contains (List_extend(List_reverse(l1), l2), Value_int(4));
+  assert [l1r_l2_contains_3']: forall l2: ListValue :: List_contains (List_reverse(List_extend(List_reverse(l1), l2)), Value_int(3));
+  assert [List_cons_extend_contains_symm]: forall x: Value, l1: ListValue, l2: ListValue ::
+    List_contains (List_extend(l1,l2), x) == List_contains (List_extend(l2,l1), x);
+  assert [contains_len]: forall l: ListValue, x: Value:: List_contains(l,x) ==> (List_len(l) >0);
+  assert [contain_remove]: forall l: ListValue, x: Value:: List_contains(l,x) ==> (List_len(l) == List_len(List_remove(l,x)) + 1);
+  assert [insert_len]: forall l: ListValue, i: int, v: Value :: List_len(List_insert(l, i, v)) == List_len(l) + 1;
+  assert [insert_contains]: forall l: ListValue, i: int, v: Value :: List_contains(List_insert(l, i, v), v);
+};
+
+procedure dict_functions_test () returns () {
+  var d1: Dict, d2: Dict, d3: Dict;
+  d1:= Dict_insert(Dict_empty(), Value_int(1), Value_int(1));
+  d2:= Dict_insert(d1, Value_bool(true), Value_int(2));
+  assert [get_1]: Dict_get(d2, Value_int(1)) == Value_int(2);
+};
+
+procedure test_dict_listconstructor () returns () {
+  var d: Dict, dl: DictList, d2: Dict, d3: Dict;
+  dl := DictList_cons(Value_bool(true), Value_int(10), DictList_cons(Value_int(1), Value_int(11), DictList_nil()));
+  d := Dict_from_DicList(dl);
+  assert [get_1]: Dict_get(d, Value_int(1)) == Value_int(11);
+  assert [get_true]: Dict_get(d, Value_bool(true)) == Value_int(11);
+  d2 := Dict_insert(Dict_insert(d, Value_int(10), Value_int(8)), Value_int(1), Value_str("abc"));
+  assert [get_true2]: Dict_get(d2, Value_bool(true)) == Value_str("abc");
+  d3 := Dict_remove(d2, Value_bool(true));
+  assert [get_1_d3]: Dict_get(d3, Value_int(1)) == Value_none();
+  assert [ncontain]: !Dict_contains(d3, Value_bool(true));
+};
+
+procedure forall_dict_test () returns () {
+  assert [ncontain_general]: forall d: Dict, k: Value :: !Dict_contains(Dict_remove(d,k), k);
+  assert [ncontain_general']: forall d: Dict, k: Value :: !Dict_contains(Dict_remove(d,normalize_value(k)), k);
+  assert [contain_general]: forall d: Dict, k: Value, v: Value :: (v == Value_none()) || Dict_contains(Dict_insert(d,k,v), k);
+  assert [remove_insert]: forall d: Dict, k: Value, v: Value, k': Value ::
+    !(Dict_get(d,k) == v) || Dict_get((Dict_insert(Dict_remove(d,k), k, v)), k') == Dict_get(d, k');
+};
+
+procedure ClassType_test() returns () {
+  var civ: Value, ci: ClassInstance, v: Value;
+  ci := ClassInstance_init_InstanceAttribute(ClassInstance_empty("point"), "x", Value_int(1));
+  ci := ClassInstance_init_InstanceAttribute(ci, "y", Value_int(2));
+  civ := Value_class (ci);
+  assert [has_x]: hasAttribute(civ,"x");
+  assert [nhas_z_expect_unknown]: hasAttribute(civ,"z");
+  assert [isInstance_class]: isInstance(civ, ValueType_class("point"));
+  assert [get_x_empty_expect_unknown]: get_InstanceAttribute(civ, "x") == ValueExcept_ok(Value_none());
+  assert [get_x]: get_InstanceAttribute(civ, "x") == ValueExcept_ok(Value_int(1));
+};
+
+#end
+
+#eval verify "cvc5" boogieTypePrelude
+--#eval boogieTypePrelude.format
+
+def Boogie.prelude : Boogie.Program :=
+   Boogie.getProgram Strata.boogieTypePrelude |>.fst
+
+end Strata
diff --git a/Strata/Languages/Python/PythonToTypeBoogie.lean b/Strata/Languages/Python/PythonToTypeBoogie.lean
new file mode 100644
index 000000000..5aad5487b
--- /dev/null
+++ b/Strata/Languages/Python/PythonToTypeBoogie.lean
@@ -0,0 +1,961 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DDM.Elab
+import Strata.DDM.AST
+import Strata.Languages.Boogie.DDMTransform.Parse
+
+import Strata.Languages.Boogie.Boogie
+import Strata.Languages.Python.PythonDialect
+import Strata.Languages.Python.FunctionSignatures
+import Strata.Languages.Python.Regex.ReToBoogie
+import Strata.Languages.Python.PyFactory
+import Strata.Languages.Python.FunctionSignatures
+import Strata.Languages.Python.BoogieTypePrelude
+import StrataTest.Transform.ProcedureInlining
+import StrataTest.Internal.InternalBoogiePrelude
+import StrataTest.Internal.InternalFunctionSignatures
+import Strata.Languages.Boogie.Verifier
+import Strata.DDM.Ion
+import Strata.Util.IO
+
+namespace Strata
+open Lambda.LTy.Syntax
+open Rat
+-- Some hard-coded things we'll need to fix later:
+
+def clientType : Boogie.Expression.Ty := .forAll [] (.tcons "Client" [])
+def dummyClient : Boogie.Expression.Expr := .fvar () "DUMMY_CLIENT" none
+
+def dictStrAnyType : Boogie.Expression.Ty := .forAll [] (.tcons "DictStrAny" [])
+def dummyDictStrAny : Boogie.Expression.Expr := .fvar () "DUMMY_DICT_STR_ANY" none
+
+def strType : Boogie.Expression.Ty := .forAll [] (.tcons "string" [])
+def dummyStr : Boogie.Expression.Expr := .fvar () "DUMMY_STR" none
+
+def listStrType : Boogie.Expression.Ty := .forAll [] (.tcons "ListStr" [])
+def dummyListStr : Boogie.Expression.Expr := .fvar () "DUMMY_LIST_STR" none
+
+def datetimeType : Boogie.Expression.Ty := .forAll [] (.tcons "Datetime" [])
+def dummyDatetime : Boogie.Expression.Expr := .fvar () "DUMMY_DATETIME" none
+
+def dateType : Boogie.Expression.Ty := .forAll [] (.tcons "Date" [])
+def dummyDate : Boogie.Expression.Expr := .fvar () "DUMMY_DATE" none
+
+def timedeltaType : Boogie.Expression.Ty := .forAll [] (.tcons "int" [])
+def dummyTimedelta : Boogie.Expression.Expr := .fvar () "DUMMY_Timedelta" none
+
+
+def ValueTy : Boogie.Expression.Ty := .forAll [] (.tcons "Value" [])
+def ClassInstanceTy : Boogie.Expression.Ty := .forAll [] (.tcons "ClassInstance" [])
+
+-------------------------------------------------------------------------------
+
+-- Translating a Python expression can require Boogie statements, e.g., a function call
+-- We translate these by first defining temporary variables to store the results of the stmts
+-- and then using those variables in the expression.
+structure PyExprTranslated where
+  stmts : List Boogie.Statement
+  expr: Boogie.Expression.Expr
+  post_stmts : List Boogie.Statement := []
+deriving Inhabited
+
+structure PythonFunctionDecl where
+  name : String
+  args : List (String × String) -- Elements are (arg_name, arg_ty) where `arg_ty` is the string representation of the type in Python
+  ret : String
+deriving Repr, BEq, Inhabited
+
+structure PythonClassDecl where
+  name : String
+  --ClassAttributes: List String
+  --InstanceAttribute: List String
+deriving Repr, BEq, Inhabited
+
+structure TranslationContext where
+  signatures : Python.Signatures
+  expectedType : Option (Lambda.LMonoTy) := none
+  variableTypes : List (String × Lambda.LMonoTy) := []
+  func_infos : List PythonFunctionDecl := []
+  class_infos : List PythonClassDecl := []
+deriving Inhabited
+
+-------------------------------------------------------------------------------
+def getFunctions (decls: List Boogie.Decl) : List String :=
+  match decls with
+  | [] => []
+  | decl::t => match decl with
+      |.func f => f.name.name :: (getFunctions t)
+      | _ => getFunctions t
+
+def PreludeFunctions : List String := getFunctions Boogie.Typeprelude.decls
+
+def create_function_app_acc (args: List Boogie.Expression.Expr) (acc: Boogie.Expression.Expr): Boogie.Expression.Expr :=
+  match args with
+  | [] => acc
+  | arg :: t => create_function_app_acc t (.app () acc arg)
+
+def create_function_app (fn: String) (args: List Boogie.Expression.Expr): Boogie.Expression.Expr :=
+  create_function_app_acc args (.op () fn none)
+
+def toPyCommands (a : Array Operation) : Array (Python.Command SourceRange) :=
+  a.map (λ op => match Python.Command.ofAst op with
+    | .error e => panic! s!"Failed to translate to Python.Command: {e}"
+    | .ok cmd => cmd)
+
+def unwrapModule (c : Python.Command SourceRange) : Array (Python.stmt SourceRange) :=
+  match c with
+  | Python.Command.Module _ body _ => body.val
+  | _ => panic! "Expected module"
+
+def strToBoogieExpr (s: String) : Boogie.Expression.Expr :=
+  .strConst () s
+
+def intToBoogieExpr (i: Int) : Boogie.Expression.Expr :=
+  .intConst () i
+
+def PyIntToInt (i : Python.int SourceRange) : Int :=
+  match i with
+  | .IntPos _ n => n.val
+  | .IntNeg _ n => -n.val
+
+def PyConstToBoogie (c: Python.constant SourceRange) : Boogie.Expression.Expr :=
+  match c with
+  | .ConString _ s => .strConst () s.val
+  | .ConPos _ i => .intConst () i.val
+  | .ConNeg _ i => .intConst () (-i.val)
+  | .ConBytes _ _b => .const () (.strConst "") -- TODO: fix
+  | .ConFloat _ f => .strConst () (f.val)
+  | .ConTrue _ => .boolConst () true
+  | .ConFalse _ => .boolConst () false
+  | _ => panic! s!"Unhandled Constant: {repr c}"
+
+def PyAliasToBoogieExpr (a : Python.alias SourceRange) : Boogie.Expression.Expr :=
+  match a with
+  | .mk_alias _ n as_n =>
+  assert! as_n.val.isNone
+  .strConst () n.val
+
+-------------------------------------------------------------------------------
+
+def strToValue (s: String) : Boogie.Expression.Expr :=
+  .app () (.op () "Value_str" none) (.strConst () s)
+
+def intToValue (i: Int) : Boogie.Expression.Expr :=
+  .app () (.op () "Value_int" none) (.intConst () i)
+
+def boolToValue (b: Bool) : Boogie.Expression.Expr :=
+  .app () (.op () "Value_bool" none) (.boolConst () b)
+
+def Value_asBool (b: Boogie.Expression.Expr) : Boogie.Expression.Expr :=
+  .app () (.op () "as_bool" none) b
+
+def strVarToValue (varname: String) : Boogie.Expression.Expr :=
+  .app () (.op () "Value_str" none) (.fvar () varname none)
+
+def intVarToValue (varname: String) : Boogie.Expression.Expr :=
+  .app () (.op () "Value_int" none) (.fvar () varname none)
+
+def boolVarToValue (varname: String) : Boogie.Expression.Expr :=
+  .app () (.op () "Value_bool" none) (.fvar () varname none)
+
+def ValueNoneExpr : Boogie.Expression.Expr :=
+  .op () "Value_none" none
+
+def classVarToValue (varname: String) : Boogie.Expression.Expr :=
+  .app () (.op () "Value_class" none) (.fvar () varname none)
+
+def emptyClassInstance (classname: String) : Boogie.Expression.Expr :=
+  .app () (.op () "ClassInstance_empty" none) (.strConst () classname)
+
+def stringToRat (s : String) : Rat :=
+  match s.toInt? with
+  | some n => n
+  | none =>
+    let parts := s.splitOn "."
+    if parts.length == 2 then
+      match parts[0]!.toInt?, parts[1]!.toNat? with
+      | some whole, some frac =>
+        (mkRat whole frac)
+      | _, _ => panic! s!"Cannot convert: {s} to Rat"
+    else panic! s!"Cannot convert: {s} to Rat"
+
+def PyConstToValue (c: Python.constant SourceRange) : Boogie.Expression.Expr :=
+  match c with
+  | .ConString _ s => strToValue s.val
+  | .ConPos _ i => intToValue i.val
+  | .ConNeg _ i => intToValue (-i.val)
+  | .ConBytes _ _b => .const () (.strConst "") -- TODO: fix
+  | .ConFloat _ f => .app () (.op () "Value_float" none) (.realConst () (stringToRat f.val))
+  | .ConTrue _ => boolToValue true
+  | .ConFalse _ => boolToValue false
+  | _ => panic! s!"Unhandled Constant: {repr c}"
+
+
+-------------------------------------------------------------------------------
+
+def handleAdd (lhs rhs: Boogie.Expression.Expr) : Boogie.Expression.Expr :=
+  .app () (.app () (.op () "Py_add_unwrap" none) lhs) rhs
+
+def handleSub (lhs rhs: Boogie.Expression.Expr) : Boogie.Expression.Expr :=
+  .app () (.app () (.op () "Py_sub_unwrap" none) lhs) rhs
+
+def handleMult (lhs rhs: Boogie.Expression.Expr) : Boogie.Expression.Expr :=
+  .app () (.app () (.op () "Py_mul_unwrap" none) lhs) rhs
+
+def handleFloorDiv (_translation_ctx: TranslationContext) (lhs rhs: Boogie.Expression.Expr) : Boogie.Expression.Expr :=
+  .app () (.app () (.op () "Int.Div" mty[int → (int → int)]) lhs) rhs
+
+def handleNot (arg: Boogie.Expression.Expr) : Boogie.Expression.Expr :=
+  (.app () (.op () "Py_not" none) arg)
+
+def handleNeg (arg: Boogie.Expression.Expr) : Boogie.Expression.Expr :=
+  (.app () (.op () "Py_neg" none) arg)
+
+def handleLt (lhs rhs: Boogie.Expression.Expr) : Boogie.Expression.Expr :=
+  .app () (.app () (.op () "Py_lt" none) lhs) rhs
+
+def handleLe (lhs rhs: Boogie.Expression.Expr) : Boogie.Expression.Expr :=
+  .app () (.app () (.op () "Py_le" none) lhs) rhs
+
+def handleGt (lhs rhs: Boogie.Expression.Expr) : Boogie.Expression.Expr :=
+  .app () (.app () (.op () "Py_gt" none) lhs) rhs
+
+def handleGe (lhs rhs: Boogie.Expression.Expr) : Boogie.Expression.Expr :=
+  .app () (.app () (.op () "Py_ge" none) lhs) rhs
+
+-------------------------------------------------------------------------------
+
+structure SubstitutionRecord where
+  pyExpr : Python.expr SourceRange
+  boogieExpr : Boogie.Expression.Expr
+
+instance : Repr (List SubstitutionRecord) where
+  reprPrec xs _ :=
+    let py_exprs := xs.map (λ r => r.pyExpr)
+    s!"{repr py_exprs}"
+
+def PyExprIdent (e1 e2: Python.expr SourceRange) : Bool :=
+  match e1, e2 with
+  | .Call sr1 _ _ _, .Call sr2 _ _ _ => sr1 == sr2
+  | _ , _ => false
+
+-- TODO: handle rest of names
+def PyListStrToBoogie (names : Array (Python.alias SourceRange)) : Boogie.Expression.Expr :=
+  .app () (.app () (.op () "ListStr_cons" mty[string → (ListStr → ListStr)]) (PyAliasToBoogieExpr names[0]!))
+       (.op () "ListStr_nil" mty[ListStr])
+
+def handleList (_elmts: Array (Python.expr SourceRange)) (expected_type : Lambda.LMonoTy): PyExprTranslated :=
+  match expected_type with
+  | (.tcons "ListStr" _) => {stmts := [], expr := (.op () "ListStr_nil" expected_type)}
+  | (.tcons "ListDictStrAny" _) => {stmts := [], expr := (.op () "ListDictStrAny_nil" expected_type)}
+  | _ => panic! s!"Unexpected type : {expected_type}"
+
+def PyOptExprToString (e : Python.opt_expr SourceRange) : String :=
+  match e with
+  | .some_expr _ (.Constant _ (.ConString _ s) _) => s.val
+  | _ => panic! "Expected some constant string: {e}"
+
+partial def PyExprToString (e : Python.expr SourceRange) : String :=
+  match e with
+  | .Name _ n _ => n.val
+  | .Attribute _ v attr _ => s!"{PyExprToString v}_{attr.val}"
+  | .Subscript _ v slice _ =>
+    let v_name := PyExprToString v
+    match v_name with
+    | "Dict" =>
+      match slice with
+      | .Tuple _ elts _ =>
+        assert! elts.val.size == 2
+        s!"Dict[{PyExprToString elts.val[0]!} {PyExprToString elts.val[1]!}]"
+      | _ => panic! s!"Unsupported slice: {repr slice}"
+    | "List" =>
+      match slice with
+      | .Name _ id _ => s!"List[{id.val}]"
+      | _ => panic! s!"Unsupported slice: {repr slice}"
+    | _ => panic! s!"Unsupported subscript to string: {repr e}"
+  | _ => panic! s!"Unhandled Expr: {repr e}"
+
+def PyExprToMonoTy (e : Python.expr SourceRange) : Lambda.LMonoTy :=
+  match e with
+  | .Name _ n _ =>
+    match n.val with
+    | "bool" => .tcons "bool" []
+    | "int" => .tcons "int" []
+    | "str" => .tcons "string" []
+    | "float" => .tcons "string" []
+    | "Dict[str Any]" => .tcons "DictStrAny" []
+    | "List[str]" => .tcons "ListStr" []
+    | "datetime" => .tcons "Datetime" []
+    | "date" => .tcons "Date" []
+    | "timedelta" => .tcons "Timedelta" []
+    | "Client" => .tcons "Client" []
+    | "LatencyAnalyzer" => .tcons "LatencyAnalyzer" []
+    | _ => panic! s!"Unhandled name: {repr e}"
+  | .Subscript _ val _slice _ =>
+    match val with
+    | .Name _ n _ =>
+      match n.val with
+      | "Dict" => .tcons "DictStrAny" []
+      | "List" => .tcons "ListStr" []
+      | _ => panic! s!"Unsupported name: {repr n}"
+    | _ => panic! s!"Expected name: {repr e}"
+  | _ => panic! s!"Unhandled Expr: {repr e}"
+
+
+-- This information should come from our prelude. For now, we use the fact that
+-- these functions are exactly the ones
+-- represented as `Call(Attribute(Name(...)))` in the AST (instead of `Call(Name(...))`).
+def callCanThrow (func_infos : List PythonFunctionDecl) (stmt: Python.stmt SourceRange) : Bool :=
+  match stmt with
+  | .Expr _ (.Call _ (.Attribute _ _ _ _) _ _) | .Assign _ _ (.Call _ (.Attribute _ _ _ _) _ _) _ => true
+  | .Expr _ (.Call _ f _ _) | .Assign _ _ (.Call _ f _ _) _ => match f with
+    | .Name _ f _ => func_infos.any (λ fi => fi.name == f.val)
+    | _ => false
+  | _ => false
+
+def noneOrExpr (translation_ctx : TranslationContext) (fname n : String) (e: Boogie.Expression.Expr) : Boogie.Expression.Expr :=
+  let type_str := translation_ctx.signatures.getFuncSigType fname n
+  if type_str.endsWith "OrNone" then
+    -- Optional param. Need to wrap e.g., string into StrOrNone
+    match type_str with
+    | "IntOrNone" => .app () (.op () "IntOrNone_mk_int" none) e
+    | "StrOrNone" => .app () (.op () "StrOrNone_mk_str" none) e
+    | "BytesOrStrOrNone" => .app () (.op () "BytesOrStrOrNone_mk_str" none) e
+    | _ => panic! "Unsupported type_str: "++ type_str
+  else
+    e
+
+def handleCallThrow (jmp_target : String) : Boogie.Statement :=
+  let cond := .eq () (.app () (.op () "ExceptOrNone_tag" none) (.fvar () "maybe_except" none)) (.op () "EN_STR_TAG" none)
+  .ite cond [.goto jmp_target] []
+
+def deduplicateTypeAnnotations (l : List (String × Option String)) : List (String × String) := Id.run do
+  let mut m : Map String String := []
+  for p in l do
+    let name := p.fst
+    let oty := p.snd
+    match oty with
+    | .some ty =>
+      match m.find? name with
+      | .some other_ty =>
+        if ty != other_ty then
+          panic! s!"Type annotation mismatch: {other_ty} vs {ty}"
+      | .none => m := (name, ty) :: m
+    | .none => ()
+  let names := l.map (λ p => p.fst)
+  let unique_names := names.dedup
+  unique_names.map (λ n =>
+    match m.find? n with
+    | .some ty => (n, ty)
+    | .none => panic s!"Missing type annotations for {n}")
+
+partial def collectVarDecls (translation_ctx : TranslationContext) (stmts: Array (Python.stmt SourceRange)) : List Boogie.Statement :=
+  let rec go (s : Python.stmt SourceRange) : List (String × Option String) :=
+    match s with
+    | .Assign _ lhs _ _ =>
+      let names := lhs.val.toList.map PyExprToString
+      names.map (λ n => (n, "Value"))
+    | .AnnAssign _ lhs ty _ _ =>
+      [(PyExprToString lhs, PyExprToString ty)]
+    | .If _ _ body _ => body.val.toList.flatMap go
+    | .For _ _ _ body _ _ => body.val.toList.flatMap go
+    | _ => []
+  let dup := stmts.toList.flatMap go
+  let dedup := deduplicateTypeAnnotations dup
+  let toBoogie (p: String × String) : List Boogie.Statement :=
+    let name := p.fst
+    let corename := name ++ "_coreval"
+    let ty_name := p.snd
+    match ty_name with
+    | "bool" => [(.init corename t[bool] (.boolConst () false)), (.havoc corename), (.init name ValueTy (boolVarToValue corename))]
+    | "str" => [(.init corename t[string] (.strConst () "")), (.havoc corename), (.init name ValueTy (strVarToValue corename))]
+    | "int" => [(.init corename t[int] (.intConst () 0)), (.havoc corename), (.init name ValueTy (intVarToValue corename))]
+    | "float" => [(.init name t[string] (.strConst () "0.0")), (.havoc name)] -- Floats as strs for now
+    | "bytes" => [(.init name t[string] (.strConst () "")), (.havoc name)]
+    | "Client" => [(.init name clientType dummyClient), (.havoc name)]
+    | "Dict[str Any]" => [(.init name dictStrAnyType dummyDictStrAny), (.havoc name)]
+    | "List[str]" => [(.init name listStrType dummyListStr), (.havoc name)]
+    | "datetime" => [(.init name datetimeType dummyDatetime), (.havoc name)]
+    | "date" => [(.init name dateType dummyDate), (.havoc name)]
+    | "timedelta" => [(.init name timedeltaType dummyTimedelta), (.havoc name)]
+    | "Value" => [(.init name ValueTy ValueNoneExpr), (.havoc name)]
+    | _ =>
+      let user_defined_class := translation_ctx.class_infos.find? (λ i => i.name == ty_name)
+      match user_defined_class with
+      | .some i =>
+        [(.init corename ClassInstanceTy (emptyClassInstance i.name) ), (.havoc corename), (.init name ValueTy (classVarToValue corename))]
+      | .none => panic! s!"Unsupported type annotation: `{ty_name}`"
+  let foo := dedup.map toBoogie
+  foo.flatten
+
+def isCall (e: Python.expr SourceRange) : Bool :=
+  match e with
+  | .Call _ _ _ _ => true
+  | _ => false
+
+def remapFname (translation_ctx: TranslationContext) (fname: String) : String :=
+  match translation_ctx.class_infos.find? (λ i => i.name == fname) with
+  | .some i =>
+    i.name ++ "___init__"
+  | _ =>
+    match fname with
+    | "float" => "str_to_float"
+    | _ => fname
+
+mutual
+
+partial def PyExprToBoogieWithSubst (translation_ctx : TranslationContext)  (substitution_records : Option (List SubstitutionRecord)) (e : Python.expr SourceRange) : PyExprTranslated :=
+  PyExprToBoogie translation_ctx e substitution_records
+
+partial def PyKWordsToBoogie (substitution_records : Option (List SubstitutionRecord)) (kw : Python.keyword SourceRange) : (String × PyExprTranslated) :=
+  match kw with
+  | .mk_keyword _ name expr =>
+    match name.val with
+    | some n => (n.val, PyExprToBoogieWithSubst default substitution_records expr)
+    | none => panic! "Keyword arg should have a name"
+
+-- TODO: we should be checking that args are right
+partial def argsAndKWordsToCanonicalList (translation_ctx : TranslationContext)
+                                 (fname: String)
+                                 (args : Array (Python.expr SourceRange))
+                                 (kwords: Array (Python.keyword SourceRange))
+                                 (substitution_records : Option (List SubstitutionRecord) := none) : List Boogie.Expression.Expr × List Boogie.Statement :=
+  if translation_ctx.func_infos.any (λ e => e.name == fname) || translation_ctx.class_infos.any (λ e => e.name++"___init__" == fname) then
+    if translation_ctx.func_infos.any (λ e => e.name == fname) then
+      (args.toList.map (λ a => (PyExprToBoogieWithSubst default substitution_records a).expr), [])
+    else
+      (args.toList.map (λ a => (PyExprToBoogieWithSubst default substitution_records a).expr), [])
+  else
+    let required_order := translation_ctx.signatures.getFuncSigOrder fname
+    assert! args.size <= required_order.length
+    let remaining := required_order.drop args.size
+    let kws_and_exprs := kwords.toList.map (PyKWordsToBoogie substitution_records)
+    let ordered_remaining_args := remaining.map (λ n => match kws_and_exprs.find? (λ p => p.fst == n) with
+      | .some p =>
+        noneOrExpr translation_ctx fname n p.snd.expr
+      | .none => Strata.Python.TypeStrToBoogieExpr (translation_ctx.signatures.getFuncSigType fname n))
+    let args := args.map (PyExprToBoogieWithSubst default substitution_records)
+    let args := (List.range required_order.length).filterMap (λ n =>
+        if n < args.size then
+          let arg_name := required_order[n]! -- Guaranteed by range. Using finRange causes breaking coercions to Nat.
+          some (noneOrExpr translation_ctx fname arg_name args[n]!.expr)
+        else
+          none)
+    (args ++ ordered_remaining_args, kws_and_exprs.flatMap (λ p => p.snd.stmts))
+
+partial def handleDict (keys: Array (Python.opt_expr SourceRange)) (values: Array (Python.expr SourceRange)) : PyExprTranslated :=
+  let dict := .app () (.op () "DictStrAny_mk" none) (.strConst () "DefaultDict") -- TODO: need to generate unique dict arg
+  assert! keys.size == values.size
+  let zipped := Array.zip keys values
+
+  let res := zipped.toList.flatMap (λ (k, v) =>
+    let n := PyOptExprToString k
+    let in_dict := (.assume s!"assume_{n}_in_dict" (.app () (.app () (.op () "str_in_dict_str_any" none) (.strConst () n)) dict))
+    match v with
+    | .Call _ f args _ =>
+      match f with
+      | .Name _ {ann := _ , val := "str"} _ =>
+        assert! args.val.size == 1
+        let dt := (.app () (.op () "datetime_to_str" none) ((PyExprToBoogie default args.val[0]!).expr))
+        let dict_of_v_is_k := (.assume s!"assume_{n}_key" (.eq () (.app () (.app () (.op () "dict_str_any_get_str" none) dict) (.strConst () n)) dt))
+        [in_dict, dict_of_v_is_k]
+      | _ => panic! "Unsupported function when constructing map"
+    | _ =>
+      let dict_of_v_is_k := (.assume s!"assume_{n}_key" (.eq () (.app () (.app () (.op () "dict_str_any_get_str" none) dict) (.strConst () n)) (.strConst () "DummyVal")))
+      [in_dict, dict_of_v_is_k])
+
+  {stmts := res , expr := dict, post_stmts := []}
+
+partial def PyExprToBoogie (translation_ctx : TranslationContext) (e : Python.expr SourceRange) (substitution_records : Option (List SubstitutionRecord) := none) : PyExprTranslated :=
+  if h : substitution_records.isSome && (substitution_records.get!.find? (λ r => PyExprIdent r.pyExpr e)).isSome then
+    have hr : (List.find? (fun r => PyExprIdent r.pyExpr e) substitution_records.get!).isSome = true := by rw [Bool.and_eq_true] at h; exact h.2
+    let record := (substitution_records.get!.find? (λ r => PyExprIdent r.pyExpr e)).get hr
+    {stmts := [], expr := record.boogieExpr}
+  else
+    match e with
+    | .Call _ f args kwords =>
+      let fn := PyExprToString f
+      if fn ∈ PreludeFunctions then
+        let trans_arg := (args.val.toList.map (λ a => (PyExprToBoogie translation_ctx a none).expr))
+        {stmts:= [], expr:= create_function_app fn trans_arg}
+      else
+        panic! s!"Call should be handled at stmt level: \n(func: {repr f}) \n(Records: {repr substitution_records}) \n(AST: {repr e.toAst})"
+    | .Constant _ c _ => {stmts := [], expr :=  PyConstToValue c}
+    | .Name _ n _ =>
+      match n.val with
+      | "AssertionError" | "Exception" => {stmts := [], expr := .strConst () n.val}
+      | s =>
+        match translation_ctx.variableTypes.find? (λ p => p.fst == s) with
+        | .some p =>
+          if translation_ctx.expectedType == some (.tcons "bool" []) && p.snd == (.tcons "DictStrAny" []) then
+            let a := .fvar () n.val none
+            let e := .app () (.op () "Bool.Not" none) (.eq () (.app () (.op () "dict_str_any_length" none) a) (.intConst () 0))
+            {stmts := [], expr := e}
+          else
+            {stmts := [], expr := .fvar () n.val none}
+        | .none => {stmts := [], expr := .fvar () n.val none}
+    | .JoinedStr _ ss => PyExprToBoogie translation_ctx ss.val[0]! -- TODO: need to actually join strings
+    | .BinOp _ lhs op rhs =>
+      let lhs := (PyExprToBoogie translation_ctx lhs)
+      let rhs := (PyExprToBoogie translation_ctx rhs)
+      match op with
+      | .Add _ =>
+        {stmts := lhs.stmts ++ rhs.stmts, expr := handleAdd lhs.expr rhs.expr}
+      | .Sub _ =>
+        {stmts := lhs.stmts ++ rhs.stmts, expr := handleSub lhs.expr rhs.expr}
+      | .Mult _ =>
+        {stmts := lhs.stmts ++ rhs.stmts, expr := handleMult lhs.expr rhs.expr}
+      | _ => panic! s!"Unhandled BinOp: {repr e}"
+    | .Compare _ lhs op rhs =>
+      let lhs := PyExprToBoogie translation_ctx lhs
+      assert! rhs.val.size == 1
+      let rhs := PyExprToBoogie translation_ctx rhs.val[0]!
+      match op.val with
+      | #[v] => match v with
+        | Strata.Python.cmpop.Eq _ =>
+          {stmts := lhs.stmts ++ rhs.stmts, expr := (.eq () lhs.expr rhs.expr)}
+        | Strata.Python.cmpop.In _ =>
+          {stmts := lhs.stmts ++ rhs.stmts, expr := .app () (.app () (.op () "str_in_dict_str_any" none) lhs.expr) rhs.expr}
+        | Strata.Python.cmpop.Lt _ =>
+          {stmts := lhs.stmts ++ rhs.stmts, expr := handleLt lhs.expr rhs.expr}
+        | Strata.Python.cmpop.LtE _ =>
+          {stmts := lhs.stmts ++ rhs.stmts, expr := handleLe lhs.expr rhs.expr}
+        | Strata.Python.cmpop.Gt _ =>
+          {stmts := lhs.stmts ++ rhs.stmts, expr := handleGt lhs.expr rhs.expr}
+        | Strata.Python.cmpop.GtE _ =>
+          {stmts := lhs.stmts ++ rhs.stmts, expr := handleGe lhs.expr rhs.expr}
+        | _ => panic! s!"Unhandled comparison op: {repr op.val}"
+      | _ => panic! s!"Unhandled comparison op: {repr op.val}"
+    | .Dict _ keys values =>
+      let res := handleDict keys.val values.val
+      res
+    | .ListComp _ keys values => panic! "ListComp must be handled at stmt level"
+    | .UnaryOp _ op arg => match op with
+      | .Not _ => {stmts := [], expr := handleNot (PyExprToBoogie translation_ctx arg).expr}
+      | _ => panic! "Unsupported UnaryOp: {repr e}"
+    | .Subscript _ v slice _ =>
+      let l := PyExprToBoogie translation_ctx v
+      let k := PyExprToBoogie translation_ctx slice
+      -- TODO: we need to plumb the type of `v` here
+      match s!"{repr l.expr}" with
+      | "LExpr.fvar () { name := \"keys\", metadata := Boogie.Visibility.unres } none" =>
+          -- let access_check : Boogie.Statement := .assert "subscript_bounds_check" (.app () (.app () (.op () "str_in_dict_str_any" none) k.expr) l.expr)
+          {stmts := l.stmts ++ k.stmts, expr := .app () (.app () (.op () "list_str_get" none) l.expr) k.expr}
+      | "LExpr.fvar () { name := \"blended_cost\", metadata := Boogie.Visibility.unres } none" =>
+          -- let access_check : Boogie.Statement := .assert "subscript_bounds_check" (.app () (.app () (.op () "str_in_dict_str_any" none) k.expr) l.expr)
+          {stmts := l.stmts ++ k.stmts, expr := .app () (.app () (.op () "dict_str_any_get_str" none) l.expr) k.expr}
+      | _ =>
+        match translation_ctx.expectedType with
+        | .some (.tcons "ListStr" []) =>
+          let access_check : Boogie.Statement := .assert "subscript_bounds_check" (.app () (.app () (.op () "str_in_dict_str_any" none) k.expr) l.expr)
+          {stmts := l.stmts ++ k.stmts ++ [access_check], expr := .app () (.app () (.op () "dict_str_any_get_list_str" none) l.expr) k.expr}
+        | _ =>
+          let access_check : Boogie.Statement := .assert "subscript_bounds_check" (.app () (.app () (.op () "str_in_dict_str_any" none) k.expr) l.expr)
+          {stmts := l.stmts ++ k.stmts ++ [access_check], expr := .app () (.app () (.op () "dict_str_any_get" none) l.expr) k.expr}
+    | .List _ elmts _ =>
+      match elmts.val[0]! with
+      | .Constant _ expr _ => match expr with
+        | .ConString _ s => handleList elmts.val (.tcons "ListStr" [])
+        | _ => panic! s!"Expr: {repr expr}"
+      | .Dict _ _ _ => handleList elmts.val (.tcons "ListDictStrAny" [])
+      | _ => panic! s!"Unexpected element: {repr elmts.val[0]!}"
+    | _ => panic! s!"Unhandled Expr: {repr e}"
+
+partial def initTmpParam (p: Python.expr SourceRange × String) : List Boogie.Statement :=
+  match p.fst with
+  | .Call _ f args _ =>
+    match f with
+    | .Name _ n _ =>
+      match n.val with
+      | "json_dumps" => [(.init p.snd t[string] (.strConst () "")), .call [p.snd, "maybe_except"] "json_dumps" [(.app () (.op () "DictStrAny_mk" none) (.strConst () "DefaultDict")), (Strata.Python.TypeStrToBoogieExpr "IntOrNone")]]
+      | "str" =>
+        assert! args.val.size == 1
+        [(.init p.snd t[string] (.strConst () "")), .set p.snd (.app () (.op () "datetime_to_str" none) ((PyExprToBoogie default args.val[0]!).expr))]
+      | "int" => [(.init p.snd t[int] (.intConst () 0)), .set p.snd (.op () "datetime_to_int" none)]
+      | _ => panic! s!"Unsupported name {n.val}"
+    | _ => panic! s!"Unsupported tmp param init call: {repr f}"
+  | _ => panic! "Expected Call"
+
+partial def exceptHandlersToBoogie (jmp_targets: List String) (translation_ctx: TranslationContext) (h : Python.excepthandler SourceRange) : List Boogie.Statement :=
+  assert! jmp_targets.length >= 2
+  match h with
+  | .ExceptHandler _ ex_ty _ body =>
+    let set_ex_ty_matches := match ex_ty.val with
+    | .some ex_ty =>
+      let inherits_from : Boogie.BoogieIdent := "inheritsFrom"
+      let get_ex_tag : Boogie.BoogieIdent := "ExceptOrNone_code_val"
+      let exception_ty : Boogie.Expression.Expr := .app () (.op () get_ex_tag none) (.fvar () "maybe_except" none)
+      let rhs_curried : Boogie.Expression.Expr := .app () (.op () inherits_from none) exception_ty
+      let res := PyExprToBoogie translation_ctx ex_ty
+      let rhs : Boogie.Expression.Expr := .app () rhs_curried (res.expr)
+      let call := .set "exception_ty_matches" rhs
+      res.stmts ++ [call]
+    | .none =>
+      [.set "exception_ty_matches" (.boolConst () false)]
+    let cond := .fvar () "exception_ty_matches" none
+    let body_if_matches := body.val.toList.flatMap (λ s => (PyStmtToBoogie jmp_targets translation_ctx s).fst) ++ [.goto jmp_targets[1]!]
+    set_ex_ty_matches ++ [.ite cond body_if_matches []]
+
+partial def handleFunctionCall (lhs: List Boogie.Expression.Ident)
+                               (fname: String)
+                               (args: Ann (Array (Python.expr SourceRange)) SourceRange)
+                               (kwords: Ann (Array (Python.keyword SourceRange)) SourceRange)
+                               (_jmp_targets: List String)
+                               (translation_ctx: TranslationContext)
+                               (_s : Python.stmt SourceRange) : List Boogie.Statement :=
+
+  let fname := remapFname translation_ctx fname
+
+  -- Boogie doesn't allow nested function calls, so we need to introduce temporary variables for each nested call
+  let nested_args_calls := args.val.filterMap (λ a => if isCall a then some a else none)
+  let args_calls_to_tmps := nested_args_calls.map (λ a => (a, s!"call_arg_tmp_{a.toAst.ann.start}"))
+  let nested_kwords_calls := kwords.val.filterMap (λ a =>
+    let arg := match a with
+      | .mk_keyword _ _ f => f
+    if isCall arg then some arg else none)
+  let kwords_calls_to_tmps := nested_kwords_calls.map (λ a => (a, s!"call_kword_tmp_{a.toAst.ann.start}"))
+
+  let substitution_records : List SubstitutionRecord := args_calls_to_tmps.toList.map (λ p => {pyExpr := p.fst, boogieExpr := .fvar () p.snd none}) ++
+                                                        kwords_calls_to_tmps.toList.map (λ p => {pyExpr := p.fst, boogieExpr := .fvar () p.snd none})
+  let res := argsAndKWordsToCanonicalList translation_ctx fname args.val kwords.val substitution_records
+  args_calls_to_tmps.toList.flatMap initTmpParam ++
+    kwords_calls_to_tmps.toList.flatMap initTmpParam ++
+    res.snd ++ [.call lhs fname res.fst]
+
+partial def handleComprehension (lhs: Python.expr SourceRange) (gen: Array (Python.comprehension SourceRange)) : List Boogie.Statement :=
+  assert! gen.size == 1
+  match gen[0]! with
+  | .mk_comprehension _ _ itr _ _ =>
+    let res := PyExprToBoogie default itr
+    let guard := .app () (.op () "Bool.Not" none) (.eq () (.app () (.op () "dict_str_any_length" none) res.expr) (.intConst () 0))
+    let then_ss: List Boogie.Statement := [.havoc (PyExprToString lhs)]
+    let else_ss: List Boogie.Statement := [.set (PyExprToString lhs) (.op () "ListStr_nil" none)]
+    res.stmts ++ [.ite guard then_ss else_ss]
+
+partial def PyStmtToBoogie (jmp_targets: List String) (translation_ctx : TranslationContext) (s : Python.stmt SourceRange) : List Boogie.Statement × TranslationContext :=
+  assert! jmp_targets.length > 0
+  let non_throw : List Boogie.Statement × Option (String × Lambda.LMonoTy) := match s with
+    | .Import _ names =>
+      ([.call [] "import" [PyListStrToBoogie names.val]], none)
+    | .ImportFrom _ s names i =>
+      let n := match s.val with
+      | some s => [strToBoogieExpr s.val]
+      | none => []
+      let i := match i.val with
+      | some i => [intToBoogieExpr (PyIntToInt i)]
+      | none => []
+      ([.call [] "importFrom" (n ++ [PyListStrToBoogie names.val] ++ i)], none)
+    | .Expr _ (.Call _ func args kwords) =>
+      let fname := PyExprToString func
+      if callCanThrow translation_ctx.func_infos s then
+        (handleFunctionCall ["maybe_except"] fname args kwords jmp_targets translation_ctx s, none)
+      else
+        (handleFunctionCall [] fname args kwords jmp_targets translation_ctx s, none)
+    | .Expr _ (.Constant _ (.ConString _ _) _) =>
+      -- TODO: Check that it's a doc string
+      ([], none) -- Doc string
+    | .Expr _ _ =>
+      panic! s!"Can't handle Expr statements that aren't calls: {repr s}"
+    | .Assign _ lhs (.Call _ func args kwords) _ =>
+      assert! lhs.val.size == 1
+      let fname := PyExprToString func
+      (handleFunctionCall [PyExprToString lhs.val[0]!, "maybe_except"] fname args kwords jmp_targets translation_ctx s, none)
+    | .Assign _ lhs rhs _ =>
+      assert! lhs.val.size == 1
+      let res := PyExprToBoogie translation_ctx rhs
+      (res.stmts ++ [.set (PyExprToString lhs.val[0]!) res.expr], none)
+    | .AnnAssign _ lhs ty { ann := _ , val := (.some (.Call _ func args kwords))} _ =>
+      let fname := PyExprToString func
+      (handleFunctionCall [PyExprToString lhs, "maybe_except"] fname args kwords jmp_targets translation_ctx s, some (PyExprToString lhs, PyExprToMonoTy ty))
+    | .AnnAssign _ lhs ty { ann := _ , val := (.some (.ListComp _ _ gen))} _ =>
+      (handleComprehension lhs gen.val, some (PyExprToString lhs, PyExprToMonoTy ty))
+    | .AnnAssign _ lhs ty {ann := _, val := (.some e)} _ =>
+      let res := (PyExprToBoogie {translation_ctx with expectedType := PyExprToMonoTy ty} e)
+      (res.stmts ++ [.set (PyExprToString lhs) res.expr], some (PyExprToString lhs, PyExprToMonoTy ty))
+    | .Try _ body handlers _orelse _finalbody =>
+        let new_target := s!"excepthandlers_{jmp_targets[0]!}"
+        let entry_except_handlers := [.block new_target []]
+        let new_jmp_stack := new_target :: jmp_targets
+        let except_handlers := handlers.val.toList.flatMap (exceptHandlersToBoogie new_jmp_stack translation_ctx)
+        let var_decls := collectVarDecls translation_ctx body.val
+        ([.block "try_block" (var_decls ++ body.val.toList.flatMap (λ s => (PyStmtToBoogie new_jmp_stack translation_ctx s).fst) ++ entry_except_handlers ++ except_handlers)], none)
+    | .FunctionDef _ _ _ _ _ _ _ _ => panic! "Can't translate FunctionDef to Boogie statement"
+    | .If _ test then_b else_b =>
+      let guard_ctx := {translation_ctx with expectedType := some (.tcons "bool" [])}
+      ([.ite (Value_asBool (PyExprToBoogie guard_ctx test).expr) (ArrPyStmtToBoogie translation_ctx then_b.val).fst (ArrPyStmtToBoogie translation_ctx else_b.val).fst], none)
+    | .Return _ v =>
+      match v.val with
+      | .some v => ([.set "ret" (PyExprToBoogie translation_ctx v).expr, .goto jmp_targets[0]!], none) -- TODO: need to thread return value name here. For now, assume "ret"
+      | .none => ([.goto jmp_targets[0]!], none)
+    | .For _ tgt itr body _ _ =>
+      -- Do one unrolling:
+      let guard := .app () (.op () "Bool.Not" none) (.eq () (.app () (.op () "dict_str_any_length" none) (PyExprToBoogie default itr).expr) (.intConst () 0))
+      match tgt with
+      | .Name _ n _ =>
+        let assign_tgt := [(.init n.val dictStrAnyType dummyDictStrAny)]
+        ([.ite guard (assign_tgt ++ (ArrPyStmtToBoogie translation_ctx body.val).fst) []], none)
+      | _ => panic! s!"tgt must be single name: {repr tgt}"
+      -- TODO: missing havoc
+    | .While _ test body _ =>
+      -- Do one unrolling:
+      let guard := .app () (.op () "Bool.Not" none) (.eq () (.app () (.op () "dict_str_any_length" none) (PyExprToBoogie default test).expr) (.intConst () 0))
+      ([.ite guard (ArrPyStmtToBoogie translation_ctx body.val).fst []], none)
+      -- TODO: missing havoc
+    | .Assert pos a _ =>
+      let res := PyExprToBoogie translation_ctx a
+      let assertname := s!"py_assertion_{pos.start}_{pos.stop}"
+      ([(.assert assertname res.expr)], none)
+    | .AugAssign _ lhs op rhs =>
+      match op with
+      | .Add _ =>
+        match lhs with
+        | .Name _ n _ =>
+          let rhs := PyExprToBoogie translation_ctx rhs
+          let new_lhs := (.strConst () "DUMMY_FLOAT")
+          (rhs.stmts ++ [.set n.val new_lhs], none)
+        | _ => panic! s!"Expected lhs to be name: {repr lhs}"
+      | .FloorDiv _ =>
+        match lhs with
+        | .Name _ n _ =>
+          let lhs := PyExprToBoogie translation_ctx lhs
+          let rhs := PyExprToBoogie translation_ctx rhs
+          let new_lhs := .app () (.app () (.op () "Int.Div" mty[int → (int → int)]) lhs.expr) rhs.expr
+          (rhs.stmts ++ [.set n.val new_lhs], none)
+        | _ => panic! s!"Expected lhs to be name: {repr lhs}"
+      | _ => panic! s!"Unsupported AugAssign op: {repr op}"
+    | _ =>
+      panic! s!"Unsupported {repr s}"
+  let new_translation_ctx := match non_throw.snd with
+  | .some s => {translation_ctx with variableTypes := s :: translation_ctx.variableTypes}
+  | .none => translation_ctx
+  if callCanThrow translation_ctx.func_infos s then
+    (non_throw.fst ++ [handleCallThrow jmp_targets[0]!], new_translation_ctx)
+  else
+    (non_throw.fst, new_translation_ctx)
+
+partial def ArrPyStmtToBoogie (translation_ctx: TranslationContext) (a : Array (Python.stmt SourceRange)) : (List Boogie.Statement × TranslationContext) :=
+  a.foldl (fun (stmts, ctx) stmt =>
+    let (newStmts, newCtx) := PyStmtToBoogie ["end"] ctx stmt
+    (stmts ++ newStmts, newCtx)
+  ) ([], translation_ctx)
+
+end --mutual
+
+
+def translateFunctions (a : Array (Python.stmt SourceRange)) (translation_ctx: TranslationContext) : List Boogie.Decl :=
+  a.toList.filterMap (λ s => match s with
+    | .FunctionDef _ name _args body _ _ret _ _ =>
+
+      let varDecls : List Boogie.Statement := []
+      let proc : Boogie.Procedure := {
+        header := {
+               name := name.val,
+               typeArgs := [],
+               inputs := [],
+               outputs := [("maybe_except", (.tcons "ExceptOrNone" []))]},
+        spec := default,
+        body := varDecls ++ (ArrPyStmtToBoogie translation_ctx body.val).fst ++ [.block "end" []]
+      }
+      some (.proc proc)
+    | _ => none)
+
+def isSubstring (needle : String) (haystack : String) : Bool :=
+  let needleLen := needle.length
+  let haystackLen := haystack.length
+  if needleLen > haystackLen then false
+  else
+    (List.range (haystackLen - needleLen + 1)).any fun i =>
+      String.Pos.Raw.extract haystack ⟨i⟩  ⟨i + needleLen⟩ == needle
+
+def IsOrType (ty_str: String) : Bool := isSubstring "Or" ty_str
+
+def pyTyStrToLMonoTy (ty_str: String) : Lambda.LMonoTy :=
+  match ty_str with
+  | "str" => mty[string]
+  | "int" => mty[int]
+  | "bool" => mty[bool]
+  | "datetime" => (.tcons "Datetime" [])
+  | _ =>
+    if IsOrType ty_str then (.tcons "Value" []) else
+      panic! s!"Unsupported type: {ty_str}"
+
+def arg_typecheck_assertion (var: String) (ty_str: String) : Boogie.Expression.Expr :=
+  match ty_str.toLower with
+  | "str" => .app () (.op () "isStr" none) (.fvar () var none)
+  | "int" => .app () (.op () "isInt" none) (.fvar () var none)
+  | "bool" => .app () (.op () "isBool" none) (.fvar () var none)
+  | "datetime" => .app () (.op () "isDatetime" none) (.fvar () var none)
+  | "none" => .app () (.op () "isNone" none) (.fvar () var none)
+  | _ => panic! s!"Unsupported type: {ty_str}"
+
+def arg_typecheck_or_expr (var: String) (ty_strs: List String) : Boogie.Expression.Expr :=
+  match ty_strs with
+  | [] => panic! "ty_strs cannot be empty"
+  | [ty] => arg_typecheck_assertion var ty
+  | ty::tys => .app () (.app () (.op () "Bool.Or" none) (arg_typecheck_assertion var ty)) (arg_typecheck_or_expr var tys)
+
+def getArg_typecheck_assertions (var: String) (ty: String) : Boogie.Statement :=
+  let typelist := ty.splitOn "Or"
+  let assertionname := var ++ "_typeconstraint"
+  if IsOrType ty then
+    .assert assertionname (arg_typecheck_or_expr var typelist)
+  else .assert assertionname (arg_typecheck_assertion var ty)
+
+def getArgs_typecheck_assertions (args: List (String × String)) : List Boogie.Statement :=
+  match args with
+  | [] => []
+  | (var, typ)::t => (getArg_typecheck_assertions var typ) :: (getArgs_typecheck_assertions t)
+
+def getArg_typecheck_precond (var: String) (ty: String) : (Boogie.BoogieLabel × Boogie.Procedure.Check) :=
+  let typelist := ty.splitOn "Or"
+  let assertionname := var ++ "_typeconstraint"
+  if IsOrType ty then
+    (assertionname, {expr:=arg_typecheck_or_expr var typelist})
+  else (assertionname, {expr:=arg_typecheck_assertion var ty})
+
+def getArgs_typecheck_preconds (args: List (String × String)) : ListMap Boogie.BoogieLabel Boogie.Procedure.Check :=
+  match args with
+  | [] => []
+  | (var, typ)::t => (getArg_typecheck_precond var typ) :: (getArgs_typecheck_preconds t)
+
+def pythonFuncToBoogie (name : String) (args: List (String × String)) (body: Array (Python.stmt SourceRange))
+      (ret : Option (Python.expr SourceRange)) (spec : Boogie.Procedure.Spec) (translation_ctx : TranslationContext) : Boogie.Procedure :=
+  let inputs : List (Lambda.Identifier Boogie.Visibility × Lambda.LMonoTy) := args.map (λ p => (p.fst, (.tcons "Value" [])))
+  let varDecls := collectVarDecls translation_ctx body
+  --++ [(.init "exception_ty_matches" t[bool] (.boolConst () false)), (.havoc "exception_ty_matches")]
+  let arg_typecheck := getArgs_typecheck_preconds args
+  let newspec := {spec with preconditions:= arg_typecheck ++ spec.preconditions}
+  let stmts := (ArrPyStmtToBoogie translation_ctx body).fst
+  let body := varDecls ++ stmts ++ [.block "end" []]
+  let constructor := name.endsWith "___init__"
+  let outputs : Lambda.LMonoTySignature := if not constructor then
+    [("ret", (.tcons "Value" [])), ("maybe_except", (.tcons "ExceptOrNone" []))]
+  else
+    let class_ty_name := name.dropRight ("___init__".length)
+    [("ret", (.tcons s!"{class_ty_name}" [])), ("maybe_except", (.tcons "ExceptOrNone" []))]
+  {
+    header := {name,
+               typeArgs := [],
+               inputs,
+               outputs},
+    spec:=newspec,
+    body
+  }
+
+def unpackPyArguments (args: Python.arguments SourceRange) : List (String × String) :=
+-- Python AST:
+-- arguments = (arg* posonlyargs, arg* args, arg? vararg, arg* kwonlyargs,
+--                  expr* kw_defaults, arg? kwarg, expr* defaults)
+  match args with -- TODO: Error if any other types of args
+  | .mk_arguments _ _ args _ _ _ _ _ =>
+    let combined := args.val
+    combined.toList.filterMap (λ a =>
+    match a with
+    | .mk_arg _ name oty _ =>
+      if name.val == "self" then
+        none
+      else
+        match oty.val with
+        | .some ty => some (name.val, PyExprToString ty)
+        | _ => panic! s!"Missing type annotation on arg: {repr a} ({repr args})")
+
+def PyFuncDefToBoogie (s: Python.stmt SourceRange) (translation_ctx: TranslationContext) : List Boogie.Decl × PythonFunctionDecl :=
+  match s with
+  | .FunctionDef _ name args body _ ret _ _ =>
+    let args := unpackPyArguments args
+    ([.proc (pythonFuncToBoogie name.val args body.val ret.val default translation_ctx)], {name := name.val, args, ret := s!"{repr ret}"})
+  | _ => panic! s!"Expected function def: {repr s}"
+
+def PyClassDefToBoogie (s: Python.stmt SourceRange) (translation_ctx: TranslationContext) : List Boogie.Decl × PythonClassDecl :=
+  match s with
+  | .ClassDef _ c_name _ _ body _ _ =>
+    let member_fn_defs := body.val.toList.filterMap (λ s => match s with
+      | .FunctionDef _ name args body _ ret _ _ => some (name, args, body, ret)
+      | _ => none)
+    (member_fn_defs.map (λ f =>
+      let name := f.fst.val
+      let args := unpackPyArguments f.snd.fst
+      let body := f.snd.snd.fst.val
+      let ret := f.snd.snd.snd.val
+      .proc (pythonFuncToBoogie (c_name.val++"_"++name) args body ret default translation_ctx)), {name := c_name.val})
+  | _ => panic! s!"Expected function def: {repr s}"
+
+def pythonToBoogie (pgm: Strata.Program): Boogie.Program :=
+  let pyCmds := toPyCommands pgm.commands
+  assert! pyCmds.size == 1
+  let insideMod := unwrapModule pyCmds[0]!
+  let func_defs := insideMod.filter (λ s => match s with
+  | .FunctionDef _ _ _ _ _ _ _ _ => true
+  | _ => false)
+
+  let class_defs := insideMod.filter (λ s => match s with
+  | .ClassDef _ _ _ _ _ _ _ => true
+  | _ => false)
+
+  let non_func_blocks := insideMod.filter (λ s => match s with
+  | .FunctionDef _ _ _ _ _ _ _ _ => false
+  | .ClassDef _ _ _ _ _ _ _ => false
+  | _ => true)
+
+  let globals := [(.var "__name__" (.forAll [] mty[string]) (.strConst () "__main__"))]
+
+  let rec helper {α : Type} (f : Python.stmt SourceRange → TranslationContext → List Boogie.Decl × α)
+               (update : TranslationContext → α → TranslationContext)
+               (acc : TranslationContext) :
+               List (Python.stmt SourceRange) → List Boogie.Decl × TranslationContext
+  | [] => ([], acc)
+  | x :: xs =>
+    let (y, info) := f x acc
+    let new_acc := update acc info
+    let (ys, acc'') := helper f update new_acc xs
+    (y ++ ys, acc'')
+
+  let func_defs_and_infos := helper PyFuncDefToBoogie (fun acc info => {acc with func_infos := info :: acc.func_infos}) default func_defs.toList
+  let func_defs := func_defs_and_infos.fst
+  let func_infos := func_defs_and_infos.snd
+
+  let class_defs_and_infos := helper PyClassDefToBoogie (fun acc info => {acc with class_infos := info :: acc.class_infos}) func_infos class_defs.toList
+  let class_defs := class_defs_and_infos.fst
+  let class_infos := class_defs_and_infos.snd
+  let class_ty_decls := [(.type (.con {name := "LatencyAnalyzer", numargs := 0})) ]
+
+  {decls := globals ++ class_ty_decls ++ func_defs ++ class_defs ++ [.proc (pythonFuncToBoogie "__main__" [] non_func_blocks none default class_infos)]}
+
+
+def exitFailure {α} (message : String) : IO α := do
+  IO.eprintln (message  ++ "\n\nRun strata --help for additional help.")
+  IO.Process.exit 1
+
+def readPythonStrata (path : String) : IO Strata.Program := do
+  let bytes ← Strata.Util.readBinInputSource path
+  if ! bytes.startsWith Ion.binaryVersionMarker then
+    exitFailure s!"pyAnalyze expected Ion file"
+  match Strata.Program.fromIon Strata.Python.Python_map Strata.Python.Python.name bytes with
+  | .ok p => pure p
+  | .error msg => exitFailure msg
+
+def getBoogieProgram (path : String) : IO Boogie.Program := do
+  let pgm ← readPythonStrata path
+  let bpgm := Strata.pythonToBoogie pgm
+  return bpgm
+
+def verifyBoogieProgram (path : String) : IO Unit := do
+  let pgm ← readPythonStrata path
+  let preludePgm := Boogie.Typeprelude
+  let bpgm := Strata.pythonToBoogie pgm
+  let newPgm : Boogie.Program := { decls := preludePgm.decls ++ bpgm.decls }
+  let vcResults ← EIO.toIO (fun f => IO.Error.userError (toString f))
+       (Boogie.verify "cvc5" newPgm)
+  let mut s := ""
+  for vcResult in vcResults do
+    s := s ++ s!"\n{vcResult.obligation.label}: {Std.format vcResult.result}\n"
+  IO.println s
+
+
+end Strata
+
+#eval (Strata.verifyBoogieProgram "Strata/Languages/Python/simppy.python.st.ion")
diff --git a/StrataTest/Languages/Python/typepreludetests/BoogieTypeClassTest.lean b/StrataTest/Languages/Python/typepreludetests/BoogieTypeClassTest.lean
new file mode 100644
index 000000000..bd5112769
--- /dev/null
+++ b/StrataTest/Languages/Python/typepreludetests/BoogieTypeClassTest.lean
@@ -0,0 +1,534 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DDM.Elab
+import Strata.DDM.AST
+import Strata.Languages.Boogie.DDMTransform.Parse
+import Strata.Languages.Boogie.Verifier
+
+namespace Strata
+
+def boogieTypePrelude :=
+#strata
+program Boogie;
+
+//Generic tag for List
+type List_tag;
+const CONS : List_tag;
+const NIL : List_tag;
+axiom [list_tag_unique]: CONS != NIL;
+
+//Will be merged with BoogiePrelude.lean
+type Error;
+function Error_message (s: string): Error;
+type Error_tag;
+const OK : Error_tag;
+const ERR : Error_tag;
+axiom [error_tag_unique]: OK != ERR;
+
+// Value and ListValue types
+type Value;
+type ListValue;
+
+// Class type
+type Class;
+type AttributeValues := Map string Value;
+type ClassInstance;
+
+// Constructors
+function Value_bool (b : bool) : Value;
+function Value_int (i : int) : Value;
+function Value_float (f : real) : Value;
+function Value_str (s : string) : Value;
+function Value_none() : Value;
+function Value_exception (e : Error): Value;
+function Value_list (lv : ListValue) : Value;
+function Value_class (ci: ClassInstance) : Value;
+
+function ListValue_nil() : ListValue;
+function ListValue_cons(x0 : Value, x1 : ListValue) : ListValue;
+//Tags
+function ListValue_tag (l: ListValue) : List_tag;
+axiom [ListValue_tag_nil_def]: ListValue_tag (ListValue_nil()) == NIL;
+axiom [ListValue_tag_cons_def]: forall v: Value, vs: ListValue ::{ListValue_cons(v, vs)} ListValue_tag (ListValue_cons(v, vs)) == CONS;
+
+// Types of Value
+type ValueType;
+type ListValueType;
+const BOOL : ValueType;
+const INT : ValueType;
+const FLOAT : ValueType;
+const STR : ValueType;
+const NONE : ValueType;
+const EXCEPTION : ValueType;
+function ValueType_class(c: Class): ValueType;
+
+function isListValueType (t: ValueType): bool;
+function isClassValueType (t: ValueType): bool;
+axiom [isClassType_def]: forall c: Class :: {isClassValueType(ValueType_class(c))} isClassValueType(ValueType_class(c));
+
+function isList (v: Value): bool;
+function isClassInstance (v: Value): bool;
+
+
+//Uniqueness axioms
+axiom [unique_ValueType_bool]: BOOL != INT && BOOL != FLOAT && BOOL != STR && BOOL != NONE && BOOL != EXCEPTION && !isListValueType(BOOL) && !(isClassValueType(BOOL));
+axiom [unique_ValueType_int]: INT != STR && INT != FLOAT && INT != NONE && INT != EXCEPTION && !isListValueType(INT) && !(isClassValueType(INT));
+axiom [unique_ValueType_float]: FLOAT != STR && FLOAT != NONE && FLOAT != EXCEPTION && !isListValueType(FLOAT) && !(isClassValueType(FLOAT));
+axiom [unique_ValueType_str]: STR != NONE && STR != EXCEPTION && !isListValueType(STR) && !(isClassValueType(STR));
+axiom [unique_ValueType_none]: NONE != EXCEPTION && !isListValueType(NONE) && !(isClassValueType(NONE));
+axiom [unique_ValueType_exception]: !isListValueType(EXCEPTION) && !(isClassValueType(EXCEPTION));
+axiom [classtype_ne_listtype]: forall t: ValueType :: {isListValueType (t), isClassValueType (t)} !(isListValueType (t) && isClassValueType (t));
+axiom [all_ValueType_cases]: forall t: ValueType ::
+  t == BOOL ||
+  t == INT ||
+  t == FLOAT ||
+  t == STR ||
+  t == NONE ||
+  t == EXCEPTION ||
+  isListValueType (t) ||
+  isClassValueType (t);
+
+//Eq axioms
+axiom [value_int_eq]: forall i: int, j: int :: {Value_int(i) == Value_int(j)} (Value_int(i) == Value_int(j)) == (i == j);
+axiom [value_bool_eq]: forall b1: bool, b2: bool :: {Value_bool(b1) == Value_bool(b2)} (Value_bool(b1) == Value_bool(b2)) == (b1 == b2);
+axiom [value_float_eq]: forall r1: real, r2: real :: {Value_float(r1) == Value_float(r2)} (Value_float(r1) == Value_float(r2)) == (r1 == r2);
+axiom [value_str_eq]: forall s1: string, s2: string :: {Value_str(s1) == Value_str(s2)} (Value_str(s1) == Value_str(s2)) == (s1 == s2);
+
+//Constructors and tag functions of ListType
+function ListType_nil() : (ListValueType);
+function ListType_cons(x0 : ValueType, x1 : ListValueType) : ListValueType;
+function ValueType_List (l: ListValueType) : ValueType;
+function ListValueType_tag (l: ListValueType) : List_tag;
+axiom [ListValueType_tag_nil_def]: ListValueType_tag (ListType_nil()) == NIL;
+axiom [ListValueType_tag_cons_def]: forall t: ValueType, ts: ListValueType ::{ListType_cons(t, ts)} (ListValueType_tag (ListType_cons(t, ts)) == CONS);
+axiom [isListValueType_def]: forall l: ListValueType ::{isListValueType(ValueType_List (l))} isListValueType(ValueType_List (l));
+
+// TypeOf and TypesOf functions
+function TypeOf (v : Value) : ValueType;
+function TypesOf (v: ListValue) : ListValueType;
+// Definitions
+axiom [TypesOf_nil_def]: TypesOf(ListValue_nil()) == ListType_nil();
+axiom [TypesOf_cons_def]: forall v: Value, vs: ListValue ::{ListValue_cons(v, vs)} TypesOf(ListValue_cons(v, vs)) == ListType_cons(TypeOf(v), TypesOf(vs));
+axiom [TypeOf_list_def]: forall l: ListValue ::{Value_list(l)} TypeOf(Value_list(l)) ==  ValueType_List(TypesOf(l));
+axiom [TypeOf_bool]: forall b: bool :: {TypeOf(Value_bool(b))} TypeOf(Value_bool(b)) == BOOL;
+axiom [TypeOf_int]: forall i: int :: {Value_int(i)} TypeOf(Value_int(i)) == INT;
+axiom [TypeOf_float]: forall f: real :: {Value_float(f)} TypeOf(Value_float(f)) == FLOAT;
+axiom [TypeOf_str]: forall s: string :: {Value_str(s)} TypeOf(Value_str(s)) == STR;
+axiom [TypeOf_exception]: forall e: Error :: {Value_exception(e)} TypeOf(Value_exception(e)) == EXCEPTION;
+axiom [TypeOf_none]: TypeOf(Value_none()) == NONE;
+axiom [TypeOf_list]: forall l: ListValue :: {Value_list(l)} TypeOf(Value_list(l)) == ValueType_List(TypesOf(l));
+
+axiom [TypeOf_bool_exists]: forall v: Value :: {TypeOf(v) == BOOL} TypeOf(v) == BOOL ==> exists b: bool :: v == Value_bool(b);
+axiom [TypeOf_int_exists]: forall v: Value :: {TypeOf(v) == INT} TypeOf(v) == INT ==> exists i: int :: v == Value_int(i);
+axiom [TypeOf_float_exists]: forall v: Value :: {TypeOf(v) == FLOAT} TypeOf(v) == FLOAT ==> exists r: real :: v == Value_float(r);
+axiom [TypeOf_string_exists]: forall v: Value :: {TypeOf(v) == STR} TypeOf(v) == STR ==> exists s: string :: v == Value_str(s);
+axiom [TypeOf_exception_exists]: forall v: Value :: {TypeOf(v) == EXCEPTION} TypeOf(v) == EXCEPTION ==> exists e: Error :: v == Value_exception(e);
+axiom [TypeOf_none']: forall v: Value :: {TypeOf(v) == NONE} (TypeOf(v) == NONE) == (v == Value_none()) ;
+axiom [TypeOf_list_exists]: forall v: Value :: {isList(v)} isList(v) ==> exists l: ListValue :: v == Value_list(l);
+axiom [TypeOf_class_exists]: forall v: Value :: {isClassInstance(v)} isClassInstance(v) ==> exists ci: ClassInstance :: v == Value_class(ci);
+
+axiom [isList_def]: forall l: ListValue :: {Value_list(l)} isList(Value_list(l));
+axiom [isList_def']: forall v: Value :: {isListValueType(TypeOf(v))} isList(v) == isListValueType(TypeOf(v));
+axiom [isClassInstance_def]: forall ci: ClassInstance :: {Value_class(ci)} isClassInstance(Value_class(ci));
+axiom [isClassInstance_def']: forall v: Value :: {isClassValueType(TypeOf(v))} isClassInstance(v) == isClassValueType(TypeOf(v));
+
+// isSubType functions
+function isSubType (t1: ValueType, t2: ValueType) : bool;
+function isSubTypes (t1: ListValueType, t2: ListValueType) : bool;
+//Definitions
+axiom [isSubTypes_nil_def]: isSubTypes(ListType_nil(), ListType_nil());
+axiom [not_isSubTypes_nil]: forall ty: ValueType, l: ListValueType :: !isSubTypes(ListType_nil(), ListType_cons(ty,l));
+axiom [not_isSubTypes_nil']: forall ty: ValueType, l: ListValueType :: !isSubTypes(ListType_cons(ty,l), ListType_nil());
+axiom [isSubTypes_cons_def]:forall t: ValueType, ts: ListValueType, t': ValueType, ts': ListValueType  ::{ListType_cons(t, ts), ListType_cons(t', ts')}
+  isSubTypes(ListType_cons(t, ts), ListType_cons(t', ts')) == (isSubType(t, t') && isSubTypes(ts, ts'));
+axiom [isSubType_list_def]: forall l: ListValueType, l': ListValueType :: {ValueType_List(l), ValueType_List(l')}
+  isSubType(ValueType_List(l), ValueType_List(l')) == isSubTypes(l, l');
+axiom [bool_substype_int]: isSubType(BOOL, INT);
+axiom [int_substype_float]: isSubType(INT, FLOAT);
+axiom [not_isSubstype_string]: forall t: ValueType ::{isSubType(STR, t), isSubType(t,STR)}
+  t == STR || (!isSubType(STR, t) && !isSubType(t,STR));
+axiom [not_isSubstype_none]: forall t: ValueType ::{isSubType(NONE, t), isSubType(NONE, t)}
+  t == NONE || (!isSubType(NONE, t) && !isSubType(t,NONE));
+axiom [not_isSubstype_exception]: forall t: ValueType ::{isSubType(EXCEPTION, t), isSubType(t, EXCEPTION)}
+  t == EXCEPTION || (!isSubType(EXCEPTION, t) && !isSubType(t, EXCEPTION));
+axiom [not_isSubstype_list]: forall t: ValueType, t': ValueType ::{isSubType(t, t')}
+  ((isListValueType(t) && !isListValueType(t')) || (!isListValueType(t) && isListValueType(t'))) ==> (!isSubType(t, t') && !isSubType(t', t));
+axiom [not_isSubstype_class_othertypes]: forall t: ValueType, t': ValueType ::{isSubType(t, t')}
+  ((isClassValueType(t) && !isClassValueType(t')) || (!isClassValueType(t) && isClassValueType(t'))) ==> (!isSubType(t, t') && !isSubType(t', t));
+axiom [not_isSubstype_class]: forall t: ValueType, c: Class ::{isSubType(ValueType_class(c), t), isSubType(t,ValueType_class(c))}
+  t != ValueType_class(c) ==> (!isSubType(ValueType_class(c), t) && !isSubType(t,ValueType_class(c)));
+// Supporting lemmas
+axiom [isSubtype_rfl]: forall t: ValueType::{isSubType (t,t)} isSubType (t,t);
+axiom [isSubtype_mono]: forall t1: ValueType, t2: ValueType ::{isSubType (t1,t2)} !isSubType (t1,t2) || (t1 == t2 || !isSubType(t2,t1));
+axiom [isSubtype_trans]: forall t1: ValueType, t2: ValueType, t3: ValueType::{isSubType(t1, t2)} !(isSubType(t1, t2) && isSubType(t2, t3)) || isSubType(t1, t3);
+
+// isInstance function:
+function isInstance (v: Value, vt: ValueType) : bool;
+axiom [isInstance_of_isSubtype]: forall v: Value, t: ValueType::{isInstance(v,t)} isInstance(v,t) == isSubType(TypeOf(v), t);
+
+function is_IntReal (v: Value) : bool;
+function Value_real_to_int (v: Value) : int;
+// to be extended
+function normalize_value (v : Value) : Value {
+  if v == Value_bool(true) then Value_int(1)
+  else (if v == Value_bool(false) then Value_int(0) else
+        if TypeOf(v) == FLOAT && is_IntReal(v) then Value_int(Value_real_to_int(v)) else
+        v)
+}
+
+// ListValue functions
+function List_contains (l : ListValue, x: Value) : bool;
+function List_len (l : ListValue) : int;
+function List_extend (l1 : ListValue, l2: ListValue) : ListValue;
+function List_append (l: ListValue, x: Value) : ListValue;
+function List_index (l : ListValue, i : int) : Value;
+function List_reverse (l: ListValue) : ListValue;
+
+//List function axioms
+axiom [List_contains_nil_def]: forall x : Value ::{List_contains(ListValue_nil(), x)}
+  !List_contains(ListValue_nil(), x);
+axiom [List_contains_cons_def]: forall x : Value, h : Value, t : ListValue ::{List_contains(ListValue_cons(h,t),x)}
+  List_contains(ListValue_cons(h,t),x) == ((normalize_value(x)==normalize_value(h)) || List_contains(t, x));
+axiom [List_len_nil_def]: List_len (ListValue_nil()) == 0;
+axiom [List_len_cons_def]: forall h : Value, t : ListValue ::{List_len (ListValue_cons(h,t))}
+  List_len (ListValue_cons(h,t)) == 1 + List_len(t);
+axiom [List_len_nonneg]: forall l: ListValue :: {List_len(l)} List_len(l) >= 0 ;
+axiom [List_extend_nil_def]: forall l1: ListValue ::{List_extend (l1, ListValue_nil())}
+  List_extend (l1, ListValue_nil()) == l1;
+axiom [List_nil_extend_def]: forall l1: ListValue ::{List_extend (ListValue_nil(), l1)}
+  List_extend (ListValue_nil(), l1) == l1;
+axiom [List_cons_extend_def]: forall h: Value, t: ListValue, l2: ListValue  ::{List_extend (ListValue_cons(h,t), l2)}
+  List_extend (ListValue_cons(h,t), l2) == ListValue_cons(h, List_extend(t,l2));
+axiom [List_cons_extend_contains]: forall x: Value, l1: ListValue, l2: ListValue  ::{List_contains (List_extend(l1,l2), x)}
+  List_contains (List_extend(l1,l2), x) == List_contains (l1,x) || List_contains(l2,x);
+axiom [List_cons_extend_contains_symm]: forall x: Value, l1: ListValue, l2: ListValue  ::{List_contains (List_extend(l1,l2), x)}
+  List_contains (List_extend(l1,l2), x) == List_contains (List_extend(l2,l1), x);
+axiom [List_len_extend]: forall l1: ListValue, l2: ListValue  ::{List_len (List_extend(l1,l2))}
+  List_len (List_extend(l1,l2)) == List_len (l1) + List_len(l2);
+axiom [List_index_nil]: forall i : int ::{List_index (ListValue_nil(), i)}
+  List_index (ListValue_nil(), i) == Value_exception(Error_message("index out of bound"));
+axiom [List_index_zero]: forall h : Value, t : ListValue ::{List_index (ListValue_cons(h,t), 0)}
+  List_index (ListValue_cons(h,t), 0) == h;
+axiom [List_index_ind]: forall h : Value, t : ListValue, i : int ::{List_index (ListValue_cons(h,t), i)}
+  (i > 0) ==> (List_index (ListValue_cons(h,t), i)) == List_index (t, i - 1);
+axiom [List_index_contains]: forall l: ListValue, i: int, x: Value :: {List_contains(l,x), List_index(l,i)}
+  (List_index(l,i) == x) ==> List_contains(l,x);
+axiom [List_index_ok]: forall l: ListValue, i: int:: {List_index(l,i)}
+  ((List_index(l,i)) != Value_exception(Error_message("index out of bound"))) == (i < List_len(l) && i >= 0);
+axiom [List_extend_get_shift]: forall l1: ListValue, l2: ListValue, i: int :: {List_extend(l2,l1)}
+  List_index(l1, i) == List_index(List_extend(l2,l1), i + List_len(l2));
+axiom [List_extend_assoc]: forall l1: ListValue, l2: ListValue, l3: ListValue :: {List_extend(List_extend(l1,l2), l3)}
+  List_extend(List_extend(l1,l2), l3) == List_extend(l1,List_extend(l2,l3));
+axiom [List_append_def]: forall l: ListValue, x: Value :: {List_append(l,x)}
+  List_append(l,x) == List_extend(l, ListValue_cons(x, ListValue_nil()));
+axiom [List_reverse_def_nil]: List_reverse(ListValue_nil()) == ListValue_nil();
+axiom [List_reverse_def_cons]: forall h: Value, t: ListValue:: {List_reverse(ListValue_cons(h,t))}
+  List_reverse(ListValue_cons(h,t)) == List_append(List_reverse(t), h);
+axiom [List_reverse_len]: forall l: ListValue :: {List_len(List_reverse(l))}
+  List_len(l) == List_len(List_reverse(l));
+axiom [List_reverse_contain]: forall l: ListValue, v: Value :: {List_contains (List_reverse(l), v)}
+  List_contains (List_reverse(l), v) == List_contains(l,v);
+axiom [List_reverse_index]: forall l: ListValue, i: int :: {List_index(List_reverse(l), i)}
+  List_index(List_reverse(l), i) == List_index(l, List_len(l)-1-i);
+axiom [List_reverse_extend]: forall l1: ListValue, l2: ListValue :: {List_reverse(List_extend(l1,l2))}
+  List_reverse(List_extend(l1,l2)) == List_extend(List_reverse(l2), List_reverse(l1));
+
+// Dict type
+type Dict := Map Value Value;
+
+//Dictionary functions
+function Dict_empty() : Dict;
+function Dict_insert (d: Dict, k: Value, v: Value) : Dict;
+function Dict_get (d: Dict, k: Value) : Value;
+function Dict_remove (d: Dict, k: Value) : Dict;
+function Dict_contains (d: Dict, k: Value) : bool;
+
+//Dictionary axioms
+axiom [emptydict_def]: forall k: Value :: {Dict_empty() [k]} Dict_empty() [k] == Value_none();
+axiom [Dict_get_def]: forall d: Dict, k: Value :: {Dict_get(d,k)} Dict_get(d,k) == d[normalize_value(k)];
+axiom [Dict_insert_def]: forall d: Dict, k: Value, v: Value :: {Dict_insert(d,k,v)} Dict_insert(d,k,v) == d[normalize_value(k):= v];
+axiom [Dict_remove_def]: forall d: Dict, k: Value :: {Dict_remove(d,k)} Dict_remove(d,k) == d[normalize_value(k):= Value_none()];
+axiom [Dict_contains_def]: forall d: Dict, k: Value :: {Dict_contains(d,k)} Dict_contains(d,k) == (Dict_get (d,k) != Value_none());
+
+// List of pairs of Value, used to construct Dict
+type DictList;
+// Constructor
+function DictList_nil(): DictList;
+function DictList_cons(k: Value, v: Value, d: DictList): DictList;
+//Tag and tag functions
+function DictList_tag (dl: DictList) : List_tag;
+axiom [DistListTag_nil_def]: DictList_tag (DictList_nil()) == NIL;
+axiom [DistListTag_cons_def]: forall k: Value, v: Value, d: DictList ::{DictList_cons(k,v,d)} DictList_tag (DictList_cons(k,v,d)) == CONS;
+// as a constructor for Dict
+function Dict_from_DicList (l : DictList) : Dict;
+function Dict_from_DicList_rev (l : DictList, acc: Dict) : Dict;
+axiom [Dict_from_DicList_rev_nil]: forall acc: Dict ::  Dict_from_DicList_rev(DictList_nil(), acc) == acc;
+axiom [Dict_from_DicList_rev_cons]: forall k: Value, v: Value, d: DictList, acc: Dict ::
+  Dict_from_DicList_rev(DictList_cons(k,v,d), acc) == Dict_from_DicList_rev(d,Dict_insert(acc, k, v));
+axiom [Dict_from_DicList_def]: forall dl: DictList:: {Dict_from_DicList(dl)}
+  Dict_from_DicList(dl) == Dict_from_DicList_rev(dl, Dict_empty());
+
+type AttributeNames;
+function AttributeNames_nil() : (AttributeNames);
+function AttributeNames_cons(x0 : string, x1 : AttributeNames) : (AttributeNames);
+function AttributeNames_tag (f: AttributeNames) : List_tag;
+function AttributeNames_contains (l : AttributeNames, x: string) : bool;
+function AttributeNames_len (l : AttributeNames) : int;
+function AttributeNames_index (l : AttributeNames, i : int) : string;
+function AttributeName_to_index (l : AttributeNames, f: string) : int;
+
+axiom [AttributeNames_len_nil_def]: AttributeNames_len (AttributeNames_nil()) == 0;
+axiom [AttributeNames_len_cons_def]: forall h : string, t : AttributeNames ::{AttributeNames_len (AttributeNames_cons(h,t))}
+  AttributeNames_len (AttributeNames_cons(h,t)) == 1 + AttributeNames_len(t);
+axiom [AttributeNames_tag_nil_def]: AttributeNames_tag(AttributeNames_nil()) == NIL;
+axiom [AttributeNames_tag_cons_def]: forall h : string, t : AttributeNames ::{} AttributeNames_tag (AttributeNames_cons(h,t)) == CONS;
+axiom [AttributeNames_contains_nil_def]: (forall x : string ::{AttributeNames_contains(AttributeNames_nil(), x)}
+  !AttributeNames_contains(AttributeNames_nil(), x));
+axiom [AttributeNames_contains_cons_def]: forall x : string, h : string, t : AttributeNames ::{AttributeNames_contains(AttributeNames_cons(h,t),x)}
+  AttributeNames_contains(AttributeNames_cons(h,t),x) == ((x==h) || AttributeNames_contains(t,x));
+axiom [AttributeNames_len_nonneg]: forall l: AttributeNames :: {AttributeNames_len(l)} AttributeNames_len(l) >= 0;
+axiom [AttributeNames_index_nil]: forall i : int ::{AttributeNames_index (AttributeNames_nil(), i)} (AttributeNames_index (AttributeNames_nil(), i)) == "";
+axiom [AttributeNames_index_zero]: forall h : string, t : AttributeNames ::{AttributeNames_index (AttributeNames_cons(h,t), 0)}
+  AttributeNames_index (AttributeNames_cons(h,t), 0) == h;
+axiom [AttributeNames_index_ind]: forall h : string, t : AttributeNames, i : int ::{AttributeNames_index (AttributeNames_cons(h,t), i)}
+  (i > 0) ==> (AttributeNames_index (AttributeNames_cons(h,t), i)) == AttributeNames_index (t, i - 1);
+axiom [AttributeNames_index_contains]: forall l: AttributeNames, i: int, x: string :: {AttributeNames_index(l,i), AttributeNames_contains(l,x)}
+  (AttributeNames_index(l,i) == x) ==> AttributeNames_contains(l,x);
+axiom [AttributeNames_index_ok]: forall l: AttributeNames, i: int:: {AttributeNames_index(l,i)}
+  ((AttributeNames_index(l,i)) != "") == (i < AttributeNames_len(l));
+axiom [AttributeName_to_index_nil_def]: forall f: string :: {AttributeName_to_index(AttributeNames_nil(), f)}
+  AttributeName_to_index(AttributeNames_nil(), f) == 0;
+axiom [AttributeName_to_index_cons_def_1]: forall h: string, t: AttributeNames :: {AttributeName_to_index(AttributeNames_cons(h,t), h)}
+  AttributeName_to_index(AttributeNames_cons(h,t), h) == 0;
+axiom [AttributeName_to_index_cons_def_2]: forall f: string, h: string, t: AttributeNames :: {AttributeName_to_index(AttributeNames_cons(h,t), f)}
+  !(h == f) ==> AttributeName_to_index(AttributeNames_cons(h,t), f) == AttributeName_to_index(t, f) + 1;
+
+function Class_mk (name: string, attributes: AttributeNames): Class;
+function Class_attributes (c: Class) : AttributeNames;
+function Class_name (c: Class): string;
+axiom [Class_attributes_def]: forall name: string, attributes: AttributeNames :: {Class_mk (name, attributes)}
+  Class_attributes(Class_mk (name, attributes)) == attributes;
+axiom [Class_name_def]: forall name: string, attributes: AttributeNames :: {Class_mk (name, attributes)}
+  Class_name(Class_mk (name, attributes)) == name;
+axiom [Class_eq_def]: forall c: Class, c': Class :: {c == c'}
+  (c == c') == (Class_name(c) == Class_name(c'));
+
+function Class_hasAttribute (c: Class, attribute: string): bool;
+axiom [Class_hasAttribute_def]: forall c: Class, attribute: string :: {Class_hasAttribute(c, attribute)}
+  Class_hasAttribute(c, attribute) == AttributeNames_contains(Class_attributes(c), attribute);
+
+function Class_err() : Class;
+axiom [Class_err_attributes_def]: Class_attributes(Class_err()) == AttributeNames_nil();
+
+function AttributeValues_empty (c: Class) : AttributeValues;
+axiom [AttributeValues_empty_def_valid]: forall c: Class, attribute: string :: {AttributeValues_empty(c)[attribute]}
+  Class_hasAttribute(c, attribute) ==> AttributeValues_empty(c)[attribute] == Value_none();
+axiom [AttributeValues_empty_def_invalid]: forall c: Class, attribute: string :: {AttributeValues_empty(c)[attribute]}
+  !Class_hasAttribute(c, attribute) ==> AttributeValues_empty(c)[attribute] == Value_exception(Error_message("Invalid Attribute of Class"));
+
+function AttributeValues_err () : AttributeValues;
+axiom [AttributeValues_err_def]: forall attribute: string :: {AttributeValues_err[attribute]}
+  AttributeValues_err()[attribute] == Value_exception(Error_message("Error ClassInstance"));
+
+function ClassInstance_mk (c: Class, av: AttributeValues) : ClassInstance;
+
+function ClassInstance_getAttributeValues (ci: ClassInstance) : AttributeValues;
+axiom [getAttributeValues_def]: forall c: Class, av: AttributeValues :: { ClassInstance_getAttributeValues(ClassInstance_mk (c, av))}
+  ClassInstance_getAttributeValues(ClassInstance_mk (c, av)) == av;
+
+function ClassInstance_getClass (ci: ClassInstance) : Class;
+axiom [get_Class_def]: forall c: Class, av: AttributeValues :: {ClassInstance_getClass(ClassInstance_mk (c, av))}
+  ClassInstance_getClass(ClassInstance_mk (c, av)) == c;
+
+axiom [TypeOf_class]: forall ci: ClassInstance :: {TypeOf(Value_class(ci))} TypeOf(Value_class(ci)) == ValueType_class(ClassInstance_getClass(ci));
+
+function ClassInstance_empty (c: Class) : ClassInstance;
+axiom [ClassInstance_mk_empty_get_attributevalues]: forall c: Class :: {ClassInstance_getAttributeValues(ClassInstance_empty (c))}
+  ClassInstance_getAttributeValues(ClassInstance_empty (c)) == AttributeValues_empty(c);
+axiom [ClassInstance_mk_empty_get_class]: forall c: Class :: {ClassInstance_getClass(ClassInstance_empty (c))}
+  ClassInstance_getClass(ClassInstance_empty (c)) == c;
+
+function ClassInstance_err (err: string) : ClassInstance;
+function ClassInstance_errortag (ci: ClassInstance): Error_tag;
+axiom [ClassInstance_err_tag]: forall err: string :: {ClassInstance_errortag(ClassInstance_err(err))}
+  ClassInstance_errortag(ClassInstance_err(err)) == ERR;
+axiom [ClassInstance_err_get_class_def]: forall err: string :: {ClassInstance_getClass(ClassInstance_err(err)) }
+  ClassInstance_getClass(ClassInstance_err(err)) == Class_err();
+axiom [ClassInstance_err_get_attributevalues_def]: forall err: string :: {ClassInstance_getAttributeValues(ClassInstance_err (err))}
+  ClassInstance_getAttributeValues(ClassInstance_err (err)) == AttributeValues_err();
+
+function ClassInstance_get_attribute(ci: ClassInstance, attribute: string) : Value;
+axiom [ClassInstance_get_attribute_def]: forall ci: ClassInstance, attribute: string ::{ClassInstance_get_attribute(ci, attribute)}
+  ClassInstance_get_attribute(ci, attribute) == ClassInstance_getAttributeValues(ci)[attribute];
+
+function ClassInstance_set_attribute (ci: ClassInstance, attribute: string, value: Value): ClassInstance;
+axiom [ClassInstance_set_attribute_def]: forall ci: ClassInstance, attribute: string, v: Value:: {ClassInstance_set_attribute(ci, attribute, v)}
+  ClassInstance_set_attribute(ci, attribute, v) == if Class_hasAttribute(ClassInstance_getClass(ci), attribute) then
+                                                      ClassInstance_mk(ClassInstance_getClass(ci), ClassInstance_getAttributeValues(ci)[attribute:=v])
+                                                  else ClassInstance_err("Set value for invalid");
+
+function get_ClassInstance (v: Value) : ClassInstance;
+axiom [get_ClassInstance_valid]: forall ci: ClassInstance :: {get_ClassInstance(Value_class(ci))}
+  get_ClassInstance(Value_class(ci)) == ci;
+axiom [get_ClassInstance_invalid]: forall v: Value :: {get_ClassInstance(v)}
+  !isClassInstance(v) ==> get_ClassInstance(v) == ClassInstance_err ("Not of Class type");
+
+function get_attribute(v: Value, attribute: string) : Value;
+axiom [get_attribute_def]: forall v: Value, attribute: string ::{get_attribute(v, attribute)}
+  get_attribute(v, attribute) == if isClassInstance(v) then
+                                    ClassInstance_get_attribute(get_ClassInstance(v), attribute)
+                                else Value_exception(Error_message("Not of Class type"));
+
+function set_attribute(v: Value, attribute: string, v': Value) : Value;
+axiom [set_attribute_def]: forall v: Value, attribute: string, v': Value ::{set_attribute(v, attribute, v')}
+  set_attribute(v, attribute, v') == if isClassInstance(v) then
+                                      Value_class(ClassInstance_set_attribute(get_ClassInstance(v), attribute, v'))
+                                    else Value_exception(Error_message("Not of Class type"));
+
+function get_Class (v: Value) : Class {
+  ClassInstance_getClass(get_ClassInstance (v))
+}
+
+function get_Class_name (v: Value) : string {
+  Class_name(ClassInstance_getClass(get_ClassInstance (v)))
+}
+
+function hasAttribute(v: Value, attribute: string): bool {
+  Class_hasAttribute (get_Class(v), attribute)
+}
+
+//Binary op function
+function int_to_real (i: int) : real;
+function str_repeat (s: string, i: int) : string;
+function Py_add (v1: Value, v2: Value) : Value;
+function Py_sub (v1: Value, v2: Value) : Value;
+function Py_mul (v1: Value, v2: Value) : Value;
+inline function bool_to_int (b: bool) : int {if b then 1 else 0}
+inline function bool_to_real (b: bool) : real {if b then 1.0 else 0.0}
+
+axiom [Py_add_ints]: forall i1: int, i2: int :: {Py_add(Value_int(i1), Value_int(i2))}
+  Py_add(Value_int(i1), Value_int(i2)) == Value_int(i1 + i2);
+axiom [Py_add_floats]: forall f1: real, f2: real :: {Py_add(Value_float(f1), Value_float(f2))}
+  Py_add(Value_float(f1), Value_float(f2)) == Value_float(f1 + f2);
+axiom [Py_add_bools]: forall b1: bool, b2: bool :: {Py_add(Value_bool(b1), Value_bool(b2))}
+  Py_add(Value_bool(b1), Value_bool(b2)) == Value_int(bool_to_int(b1) + bool_to_int(b2));
+axiom [Py_add_int_bool]: forall i: int, b: bool :: {Py_add(Value_int(i), Value_bool(b))}
+  Py_add(Value_int(i), Value_bool(b)) == Value_int(i + bool_to_int(b));
+axiom [Py_add_bool_int]: forall b: bool, i: int :: {Py_add(Value_bool(b), Value_int(i))}
+  Py_add(Value_bool(b), Value_int(i)) == Value_int(bool_to_int(b) + i);
+axiom [Py_add_int_float]: forall i: int, r: real :: {Py_add(Value_int(i), Value_float(r))}
+  Py_add(Value_int(i), Value_float(r)) == Value_float(r + int_to_real(i));
+axiom [Py_add_float_int]: forall r: real, i: int :: {Py_add(Value_float(r), Value_int(i))}
+  Py_add(Value_float(r), Value_int(i)) == Value_float(int_to_real(i) + r);
+axiom [Py_add_float_bool]: forall r: real, b: bool :: {Py_add(Value_float(r), Value_bool(b))}
+  Py_add(Value_float(r), Value_bool(b)) == Value_float(r + bool_to_real(b));
+axiom [Py_add_bool_float]: forall b: bool, r: real :: {Py_add(Value_bool(b), Value_float(r))}
+  Py_add(Value_bool(b), Value_float(r)) == Value_float(bool_to_real(b) + r);
+axiom [Py_add_strs]:forall s1: string, s2: string :: {Py_add(Value_str(s1), Value_str(s2))}
+  Py_add(Value_str(s1), Value_str(s2)) == Value_str(str.concat(s1, s2));
+axiom [Py_add_str_int]: forall s: string, i: int :: {Py_add(Value_str(s), Value_int(i))}
+  Py_add(Value_str(s), Value_int(i)) == Value_exception(Error_message("Cannot add string to int"));
+axiom [Py_add_int_str]: forall s: string, i: int :: {Py_add(Value_int(i), Value_str(s)) }
+  Py_add(Value_int(i), Value_str(s)) == Value_exception(Error_message("Cannot add string to int"));
+axiom [Py_add_str_bool]: forall s: string, b: bool :: {Py_add(Value_str(s), Value_bool(b))}
+  Py_add(Value_str(s), Value_bool(b)) == Value_exception(Error_message("Cannot add string to bool"));
+axiom [Py_add_bool_str]: forall s: string, b: bool :: {Py_add(Value_bool(b), Value_str(s))}
+  Py_add(Value_bool(b), Value_str(s)) == Value_exception(Error_message("Cannot add bool to string"));
+axiom [Py_add_unsupport]: forall v1: Value, v2: Value :: {Py_add(v1,v2)}
+  ((TypeOf(v1)!=BOOL && TypeOf(v1)!=INT && TypeOf(v1)!=FLOAT && TypeOf(v1)!=STR) ||
+  (TypeOf(v2)!=BOOL && TypeOf(v2)!=INT && TypeOf(v2)!=FLOAT && TypeOf(v2)!=STR)) ==>
+  Py_add(v1, v2) == Value_exception(Error_message("Operand Type is not supported"));
+
+axiom [Py_mul_ints]: forall i1: int, i2: int :: {Py_mul(Value_int(i1), Value_int(i2))}
+  Py_mul(Value_int(i1), Value_int(i2)) == Value_int(i1 * i2);
+axiom [Py_mul_bools]: forall b1: bool, b2: bool :: {Py_mul(Value_bool(b1), Value_bool(b2))}
+  Py_mul(Value_bool(b1), Value_bool(b2)) == Value_int(bool_to_int(b1) * bool_to_int(b2));
+axiom [Py_mul_int_bool]: forall i: int, b: bool :: {Py_mul(Value_int(i), Value_bool(b))}
+  Py_mul(Value_int(i), Value_bool(b)) == Value_int(i * bool_to_int(b));
+axiom [Py_mul_bool_int]: forall b: bool, i: int :: {Py_mul(Value_bool(b), Value_int(i))}
+  Py_mul(Value_bool(b), Value_int(i)) == Value_int(bool_to_int(b) * i);
+axiom [Py_mul_str]: forall s1: string, s2: string :: {Py_mul(Value_str(s1), Value_str(s2))}
+  Py_mul(Value_str(s1), Value_str(s2)) == Value_exception(Error_message("Cannot multiply two strings"));
+axiom [Py_mul_str_int]: forall s: string, i: int :: {Py_mul(Value_str(s), Value_int(i))}
+  Py_mul(Value_str(s), Value_int(i)) == Value_str(str_repeat(s, i));
+axiom [Py_mul_int_str]: forall s: string, i: int :: {Py_mul(Value_int(i), Value_str(s))}
+  Py_mul(Value_int(i), Value_str(s)) == Value_str(str_repeat(s, i));
+axiom [Py_mul_str_bool]: forall s: string, b: bool :: {Py_mul(Value_str(s), Value_bool(b))}
+  Py_mul(Value_str(s), Value_bool(b)) == Value_str(if b then s else "");
+axiom [Py_mul_bool_str]: forall s: string, b: bool :: {Py_mul(Value_bool(b), Value_str(s)) }
+  Py_mul(Value_bool(b), Value_str(s)) ==  Value_str(if b then s else "");
+axiom [Py_mul_unsupport]: forall v1: Value, v2: Value :: {Py_mul(v1,v2)}
+  ((TypeOf(v1)!=BOOL && TypeOf(v1)!=INT && TypeOf(v1)!=FLOAT && TypeOf(v1)!=STR) ||
+  (TypeOf(v2)!=BOOL && TypeOf(v2)!=INT && TypeOf(v2)!=FLOAT && TypeOf(v2)!=STR)) ==>
+  Py_mul(v1, v2) == Value_exception(Error_message("Operand Type is not supported"));
+
+
+//Testing
+
+procedure Class1_init (name: Value, val: Value) returns (ret: Value)
+spec {
+  requires [name_is_string]: TypeOf(name) == STR;
+  ensures [ret_is_class]: get_Class(ret) == Class_mk ("Class1", AttributeNames_cons("name", AttributeNames_cons("value", AttributeNames_nil())));
+  ensures [get_name_eq]: get_attribute(ret, "name") == name;
+  ensures [get_name_eq]: get_attribute(ret, "value") == val;
+}
+{
+  var c: Class;
+  inlined: {
+  c := Class_mk ("Class1", AttributeNames_cons("name", AttributeNames_cons("value", AttributeNames_nil())));
+  ret := Value_class(ClassInstance_empty (c));
+  ret := set_attribute(ret, "name", name);
+  ret := set_attribute(ret, "value", val);}
+};
+
+procedure Class2_init (name: Value, price: Value) returns (ret: Value)
+spec {
+  requires [name_is_string]: TypeOf(name) == STR;
+  ensures [ret_is_class]: get_Class(ret) == Class_mk ("Class2", AttributeNames_cons("name", AttributeNames_cons("price", AttributeNames_nil())));
+  ensures [get_name_eq]: get_attribute(ret, "name") == name;
+  ensures [get_name_eq]: get_attribute(ret, "price") == price;
+}
+{
+  var c: Class;
+  c := Class_mk ("Class2", AttributeNames_cons("name", AttributeNames_cons("price", AttributeNames_nil())));
+  ret := Value_class(ClassInstance_empty (c));
+  ret := set_attribute(ret, "name", name);
+  ret := set_attribute(ret, "price", price);
+};
+
+procedure get_name(v: Value) returns (name: string)
+spec {
+  requires [has_name]: hasAttribute(v, "name") && TypeOf(get_attribute(v,"name")) == STR;
+  ensures [name_eq]: get_attribute(v,"name") == Value_str(name);
+}
+{};
+
+procedure class_test(i : int) returns () {
+  var v: Value, name: string;
+  if (i > 7) {
+    call v := Class1_init(Value_str("foo"), Value_int(2));
+  } else {
+    if (i > 0) {
+    call v := Class2_init(Value_str("bar"), Value_float(2.2));
+    } else {
+      v := Value_int (5);
+    }
+  }
+  assume [i_gt_0]: i >= 1;
+  call name:= get_name (v);
+  assert [name_eq]: name == "foo" || name == "bar";
+};
+
+
+#end
+
+#eval verify "cvc5" boogieTypePrelude
+
+def Boogie.prelude : Boogie.Program :=
+   Boogie.getProgram Strata.boogieTypePrelude |>.fst
+
+end Strata
diff --git a/StrataTest/Languages/Python/typepreludetests/BoogieTypeTestSimple.lean b/StrataTest/Languages/Python/typepreludetests/BoogieTypeTestSimple.lean
new file mode 100644
index 000000000..9931d2dce
--- /dev/null
+++ b/StrataTest/Languages/Python/typepreludetests/BoogieTypeTestSimple.lean
@@ -0,0 +1,514 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DDM.Elab
+import Strata.DDM.AST
+import Strata.Languages.Boogie.DDMTransform.Parse
+import Strata.Languages.Boogie.Verifier
+
+namespace Strata
+
+def boogieTypePrelude :=
+#strata
+program Boogie;
+
+//Generic tag for List
+type List_tag;
+const CONS : List_tag;
+const NIL : List_tag;
+axiom [list_tag_unique]: CONS != NIL;
+
+//Will be merged with BoogiePrelude.lean
+type Error;
+function Error_message (s: string): Error;
+type Error_tag;
+const OK : Error_tag;
+const ERR : Error_tag;
+axiom [error_tag_unique]: OK != ERR;
+
+// Value and ListValue types
+type Value;
+type ListValue;
+
+// Class type
+type Class;
+type AttributeValues := Map string Value;
+type ClassInstance;
+
+// Constructors
+function Value_bool (b : bool) : Value;
+function Value_int (i : int) : Value;
+function Value_float (f : real) : Value;
+function Value_str (s : string) : Value;
+function Value_none() : Value;
+function Value_exception (e : Error): Value;
+function Value_list (lv : ListValue) : Value;
+function Value_class (ci: ClassInstance) : Value;
+
+function ListValue_nil() : ListValue;
+function ListValue_cons(x0 : Value, x1 : ListValue) : ListValue;
+//Tags
+function ListValue_tag (l: ListValue) : List_tag;
+axiom [ListValue_tag_nil_def]: ListValue_tag (ListValue_nil()) == NIL;
+axiom [ListValue_tag_cons_def]: forall v: Value, vs: ListValue ::{ListValue_cons(v, vs)} ListValue_tag (ListValue_cons(v, vs)) == CONS;
+
+// Types of Value
+type ValueType;
+type ListValueType;
+const BOOL : ValueType;
+const INT : ValueType;
+const FLOAT : ValueType;
+const STR : ValueType;
+const NONE : ValueType;
+const EXCEPTION : ValueType;
+function ValueType_class(c: Class): ValueType;
+
+function isListValueType (t: ValueType): bool;
+function isClassValueType (t: ValueType): bool;
+axiom [isClassType_def]: forall c: Class :: {isClassValueType(ValueType_class(c))} isClassValueType(ValueType_class(c));
+
+function isList (v: Value): bool;
+function isClassInstance (v: Value): bool;
+
+
+//Uniqueness axioms
+axiom [unique_ValueType_bool]: BOOL != INT && BOOL != FLOAT && BOOL != STR && BOOL != NONE && BOOL != EXCEPTION && !isListValueType(BOOL) && !(isClassValueType(BOOL));
+axiom [unique_ValueType_int]: INT != STR && INT != FLOAT && INT != NONE && INT != EXCEPTION && !isListValueType(INT) && !(isClassValueType(INT));
+axiom [unique_ValueType_float]: FLOAT != STR && FLOAT != NONE && FLOAT != EXCEPTION && !isListValueType(FLOAT) && !(isClassValueType(FLOAT));
+axiom [unique_ValueType_str]: STR != NONE && STR != EXCEPTION && !isListValueType(STR) && !(isClassValueType(STR));
+axiom [unique_ValueType_none]: NONE != EXCEPTION && !isListValueType(NONE) && !(isClassValueType(NONE));
+axiom [unique_ValueType_exception]: !isListValueType(EXCEPTION) && !(isClassValueType(EXCEPTION));
+axiom [classtype_ne_listtype]: forall t: ValueType :: {isListValueType (t), isClassValueType (t)} !(isListValueType (t) && isClassValueType (t));
+axiom [all_ValueType_cases]: forall t: ValueType ::
+  t == BOOL ||
+  t == INT ||
+  t == FLOAT ||
+  t == STR ||
+  t == NONE ||
+  t == EXCEPTION ||
+  isListValueType (t) ||
+  isClassValueType (t);
+
+//Eq axioms
+axiom [value_int_eq]: forall i: int, j: int :: {Value_int(i) == Value_int(j)} (Value_int(i) == Value_int(j)) == (i == j);
+axiom [value_bool_eq]: forall b1: bool, b2: bool :: {Value_bool(b1) == Value_bool(b2)} (Value_bool(b1) == Value_bool(b2)) == (b1 == b2);
+axiom [value_float_eq]: forall r1: real, r2: real :: {Value_float(r1) == Value_float(r2)} (Value_float(r1) == Value_float(r2)) == (r1 == r2);
+axiom [value_str_eq]: forall s1: string, s2: string :: {Value_str(s1) == Value_str(s2)} (Value_str(s1) == Value_str(s2)) == (s1 == s2);
+
+//Constructors and tag functions of ListType
+function ListType_nil() : (ListValueType);
+function ListType_cons(x0 : ValueType, x1 : ListValueType) : ListValueType;
+function ValueType_List (l: ListValueType) : ValueType;
+function ListValueType_tag (l: ListValueType) : List_tag;
+axiom [ListValueType_tag_nil_def]: ListValueType_tag (ListType_nil()) == NIL;
+axiom [ListValueType_tag_cons_def]: forall t: ValueType, ts: ListValueType ::{ListType_cons(t, ts)} (ListValueType_tag (ListType_cons(t, ts)) == CONS);
+axiom [isListValueType_def]: forall l: ListValueType ::{isListValueType(ValueType_List (l))} isListValueType(ValueType_List (l));
+
+// TypeOf and TypesOf functions
+function TypeOf (v : Value) : ValueType;
+function TypesOf (v: ListValue) : ListValueType;
+// Definitions
+axiom [TypesOf_nil_def]: TypesOf(ListValue_nil()) == ListType_nil();
+axiom [TypesOf_cons_def]: forall v: Value, vs: ListValue ::{ListValue_cons(v, vs)} TypesOf(ListValue_cons(v, vs)) == ListType_cons(TypeOf(v), TypesOf(vs));
+axiom [TypeOf_list_def]: forall l: ListValue ::{Value_list(l)} TypeOf(Value_list(l)) ==  ValueType_List(TypesOf(l));
+axiom [TypeOf_bool]: forall b: bool :: {TypeOf(Value_bool(b))} TypeOf(Value_bool(b)) == BOOL;
+axiom [TypeOf_int]: forall i: int :: {Value_int(i)} TypeOf(Value_int(i)) == INT;
+axiom [TypeOf_float]: forall f: real :: {Value_float(f)} TypeOf(Value_float(f)) == FLOAT;
+axiom [TypeOf_str]: forall s: string :: {Value_str(s)} TypeOf(Value_str(s)) == STR;
+axiom [TypeOf_exception]: forall e: Error :: {Value_exception(e)} TypeOf(Value_exception(e)) == EXCEPTION;
+axiom [TypeOf_none]: TypeOf(Value_none()) == NONE;
+axiom [TypeOf_list]: forall l: ListValue :: {Value_list(l)} TypeOf(Value_list(l)) == ValueType_List(TypesOf(l));
+
+axiom [TypeOf_bool_exists]: forall v: Value :: {TypeOf(v) == BOOL} TypeOf(v) == BOOL ==> exists b: bool :: v == Value_bool(b);
+axiom [TypeOf_int_exists]: forall v: Value :: {TypeOf(v) == INT} TypeOf(v) == INT ==> exists i: int :: v == Value_int(i);
+axiom [TypeOf_float_exists]: forall v: Value :: {TypeOf(v) == FLOAT} TypeOf(v) == FLOAT ==> exists r: real :: v == Value_float(r);
+axiom [TypeOf_string_exists]: forall v: Value :: {TypeOf(v) == STR} TypeOf(v) == STR ==> exists s: string :: v == Value_str(s);
+axiom [TypeOf_exception_exists]: forall v: Value :: {TypeOf(v) == EXCEPTION} TypeOf(v) == EXCEPTION ==> exists e: Error :: v == Value_exception(e);
+axiom [TypeOf_none']: forall v: Value :: {TypeOf(v) == NONE} (TypeOf(v) == NONE) == (v == Value_none()) ;
+axiom [TypeOf_list_exists]: forall v: Value :: {isList(v)} isList(v) ==> exists l: ListValue :: v == Value_list(l);
+axiom [TypeOf_class_exists]: forall v: Value :: {isClassInstance(v)} isClassInstance(v) ==> exists ci: ClassInstance :: v == Value_class(ci);
+
+axiom [isList_def]: forall l: ListValue :: {Value_list(l)} isList(Value_list(l));
+axiom [isList_def']: forall v: Value :: {isListValueType(TypeOf(v))} isList(v) == isListValueType(TypeOf(v));
+axiom [isClassInstance_def]: forall ci: ClassInstance :: {Value_class(ci)} isClassInstance(Value_class(ci));
+axiom [isClassInstance_def']: forall v: Value :: {isClassValueType(TypeOf(v))} isClassInstance(v) == isClassValueType(TypeOf(v));
+
+// isSubType functions
+function isSubType (t1: ValueType, t2: ValueType) : bool;
+function isSubTypes (t1: ListValueType, t2: ListValueType) : bool;
+//Definitions
+axiom [isSubTypes_nil_def]: isSubTypes(ListType_nil(), ListType_nil());
+axiom [not_isSubTypes_nil]: forall ty: ValueType, l: ListValueType :: !isSubTypes(ListType_nil(), ListType_cons(ty,l));
+axiom [not_isSubTypes_nil']: forall ty: ValueType, l: ListValueType :: !isSubTypes(ListType_cons(ty,l), ListType_nil());
+axiom [isSubTypes_cons_def]:forall t: ValueType, ts: ListValueType, t': ValueType, ts': ListValueType  ::{ListType_cons(t, ts), ListType_cons(t', ts')}
+  isSubTypes(ListType_cons(t, ts), ListType_cons(t', ts')) == (isSubType(t, t') && isSubTypes(ts, ts'));
+axiom [isSubType_list_def]: forall l: ListValueType, l': ListValueType :: {ValueType_List(l), ValueType_List(l')}
+  isSubType(ValueType_List(l), ValueType_List(l')) == isSubTypes(l, l');
+axiom [bool_substype_int]: isSubType(BOOL, INT);
+axiom [int_substype_float]: isSubType(INT, FLOAT);
+axiom [not_isSubstype_string]: forall t: ValueType ::{isSubType(STR, t), isSubType(t,STR)}
+  t == STR || (!isSubType(STR, t) && !isSubType(t,STR));
+axiom [not_isSubstype_none]: forall t: ValueType ::{isSubType(NONE, t), isSubType(NONE, t)}
+  t == NONE || (!isSubType(NONE, t) && !isSubType(t,NONE));
+axiom [not_isSubstype_exception]: forall t: ValueType ::{isSubType(EXCEPTION, t), isSubType(t, EXCEPTION)}
+  t == EXCEPTION || (!isSubType(EXCEPTION, t) && !isSubType(t, EXCEPTION));
+axiom [not_isSubstype_list]: forall t: ValueType, t': ValueType ::{isSubType(t, t')}
+  ((isListValueType(t) && !isListValueType(t')) || (!isListValueType(t) && isListValueType(t'))) ==> (!isSubType(t, t') && !isSubType(t', t));
+axiom [not_isSubstype_class_othertypes]: forall t: ValueType, t': ValueType ::{isSubType(t, t')}
+  ((isClassValueType(t) && !isClassValueType(t')) || (!isClassValueType(t) && isClassValueType(t'))) ==> (!isSubType(t, t') && !isSubType(t', t));
+axiom [not_isSubstype_class]: forall t: ValueType, c: Class ::{isSubType(ValueType_class(c), t), isSubType(t,ValueType_class(c))}
+  t != ValueType_class(c) ==> (!isSubType(ValueType_class(c), t) && !isSubType(t,ValueType_class(c)));
+// Supporting lemmas
+axiom [isSubtype_rfl]: forall t: ValueType::{isSubType (t,t)} isSubType (t,t);
+axiom [isSubtype_mono]: forall t1: ValueType, t2: ValueType ::{isSubType (t1,t2)} !isSubType (t1,t2) || (t1 == t2 || !isSubType(t2,t1));
+axiom [isSubtype_trans]: forall t1: ValueType, t2: ValueType, t3: ValueType::{isSubType(t1, t2)} !(isSubType(t1, t2) && isSubType(t2, t3)) || isSubType(t1, t3);
+
+// isInstance function:
+function isInstance (v: Value, vt: ValueType) : bool;
+axiom [isInstance_of_isSubtype]: forall v: Value, t: ValueType::{isInstance(v,t)} isInstance(v,t) == isSubType(TypeOf(v), t);
+
+function is_IntReal (v: Value) : bool;
+function Value_real_to_int (v: Value) : int;
+// to be extended
+function normalize_value (v : Value) : Value {
+  if v == Value_bool(true) then Value_int(1)
+  else (if v == Value_bool(false) then Value_int(0) else
+        if TypeOf(v) == FLOAT && is_IntReal(v) then Value_int(Value_real_to_int(v)) else
+        v)
+}
+
+// ListValue functions
+function List_contains (l : ListValue, x: Value) : bool;
+function List_len (l : ListValue) : int;
+function List_extend (l1 : ListValue, l2: ListValue) : ListValue;
+function List_append (l: ListValue, x: Value) : ListValue;
+function List_index (l : ListValue, i : int) : Value;
+function List_reverse (l: ListValue) : ListValue;
+
+//List function axioms
+axiom [List_contains_nil_def]: forall x : Value ::{List_contains(ListValue_nil(), x)}
+  !List_contains(ListValue_nil(), x);
+axiom [List_contains_cons_def]: forall x : Value, h : Value, t : ListValue ::{List_contains(ListValue_cons(h,t),x)}
+  List_contains(ListValue_cons(h,t),x) == ((normalize_value(x)==normalize_value(h)) || List_contains(t, x));
+axiom [List_len_nil_def]: List_len (ListValue_nil()) == 0;
+axiom [List_len_cons_def]: forall h : Value, t : ListValue ::{List_len (ListValue_cons(h,t))}
+  List_len (ListValue_cons(h,t)) == 1 + List_len(t);
+axiom [List_len_nonneg]: forall l: ListValue :: {List_len(l)} List_len(l) >= 0 ;
+axiom [List_extend_nil_def]: forall l1: ListValue ::{List_extend (l1, ListValue_nil())}
+  List_extend (l1, ListValue_nil()) == l1;
+axiom [List_nil_extend_def]: forall l1: ListValue ::{List_extend (ListValue_nil(), l1)}
+  List_extend (ListValue_nil(), l1) == l1;
+axiom [List_cons_extend_def]: forall h: Value, t: ListValue, l2: ListValue  ::{List_extend (ListValue_cons(h,t), l2)}
+  List_extend (ListValue_cons(h,t), l2) == ListValue_cons(h, List_extend(t,l2));
+axiom [List_cons_extend_contains]: forall x: Value, l1: ListValue, l2: ListValue  ::{List_contains (List_extend(l1,l2), x)}
+  List_contains (List_extend(l1,l2), x) == List_contains (l1,x) || List_contains(l2,x);
+axiom [List_cons_extend_contains_symm]: forall x: Value, l1: ListValue, l2: ListValue  ::{List_contains (List_extend(l1,l2), x)}
+  List_contains (List_extend(l1,l2), x) == List_contains (List_extend(l2,l1), x);
+axiom [List_len_extend]: forall l1: ListValue, l2: ListValue  ::{List_len (List_extend(l1,l2))}
+  List_len (List_extend(l1,l2)) == List_len (l1) + List_len(l2);
+axiom [List_index_nil]: forall i : int ::{List_index (ListValue_nil(), i)}
+  List_index (ListValue_nil(), i) == Value_exception(Error_message("index out of bound"));
+axiom [List_index_zero]: forall h : Value, t : ListValue ::{List_index (ListValue_cons(h,t), 0)}
+  List_index (ListValue_cons(h,t), 0) == h;
+axiom [List_index_ind]: forall h : Value, t : ListValue, i : int ::{List_index (ListValue_cons(h,t), i)}
+  (i > 0) ==> (List_index (ListValue_cons(h,t), i)) == List_index (t, i - 1);
+axiom [List_index_contains]: forall l: ListValue, i: int, x: Value :: {List_contains(l,x), List_index(l,i)}
+  (List_index(l,i) == x) ==> List_contains(l,x);
+axiom [List_index_ok]: forall l: ListValue, i: int:: {List_index(l,i)}
+  ((List_index(l,i)) != Value_exception(Error_message("index out of bound"))) == (i < List_len(l) && i >= 0);
+axiom [List_extend_get_shift]: forall l1: ListValue, l2: ListValue, i: int :: {List_extend(l2,l1)}
+  List_index(l1, i) == List_index(List_extend(l2,l1), i + List_len(l2));
+axiom [List_extend_assoc]: forall l1: ListValue, l2: ListValue, l3: ListValue :: {List_extend(List_extend(l1,l2), l3)}
+  List_extend(List_extend(l1,l2), l3) == List_extend(l1,List_extend(l2,l3));
+axiom [List_append_def]: forall l: ListValue, x: Value :: {List_append(l,x)}
+  List_append(l,x) == List_extend(l, ListValue_cons(x, ListValue_nil()));
+axiom [List_reverse_def_nil]: List_reverse(ListValue_nil()) == ListValue_nil();
+axiom [List_reverse_def_cons]: forall h: Value, t: ListValue:: {List_reverse(ListValue_cons(h,t))}
+  List_reverse(ListValue_cons(h,t)) == List_append(List_reverse(t), h);
+axiom [List_reverse_len]: forall l: ListValue :: {List_len(List_reverse(l))}
+  List_len(l) == List_len(List_reverse(l));
+axiom [List_reverse_contain]: forall l: ListValue, v: Value :: {List_contains (List_reverse(l), v)}
+  List_contains (List_reverse(l), v) == List_contains(l,v);
+axiom [List_reverse_index]: forall l: ListValue, i: int :: {List_index(List_reverse(l), i)}
+  List_index(List_reverse(l), i) == List_index(l, List_len(l)-1-i);
+axiom [List_reverse_extend]: forall l1: ListValue, l2: ListValue :: {List_reverse(List_extend(l1,l2))}
+  List_reverse(List_extend(l1,l2)) == List_extend(List_reverse(l2), List_reverse(l1));
+
+// Dict type
+type Dict := Map Value Value;
+
+//Dictionary functions
+function Dict_empty() : Dict;
+function Dict_insert (d: Dict, k: Value, v: Value) : Dict;
+function Dict_get (d: Dict, k: Value) : Value;
+function Dict_remove (d: Dict, k: Value) : Dict;
+function Dict_contains (d: Dict, k: Value) : bool;
+
+//Dictionary axioms
+axiom [emptydict_def]: forall k: Value :: {Dict_empty() [k]} Dict_empty() [k] == Value_none();
+axiom [Dict_get_def]: forall d: Dict, k: Value :: {Dict_get(d,k)} Dict_get(d,k) == d[normalize_value(k)];
+axiom [Dict_insert_def]: forall d: Dict, k: Value, v: Value :: {Dict_insert(d,k,v)} Dict_insert(d,k,v) == d[normalize_value(k):= v];
+axiom [Dict_remove_def]: forall d: Dict, k: Value :: {Dict_remove(d,k)} Dict_remove(d,k) == d[normalize_value(k):= Value_none()];
+axiom [Dict_contains_def]: forall d: Dict, k: Value :: {Dict_contains(d,k)} Dict_contains(d,k) == (Dict_get (d,k) != Value_none());
+
+// List of pairs of Value, used to construct Dict
+type DictList;
+// Constructor
+function DictList_nil(): DictList;
+function DictList_cons(k: Value, v: Value, d: DictList): DictList;
+//Tag and tag functions
+function DictList_tag (dl: DictList) : List_tag;
+axiom [DistListTag_nil_def]: DictList_tag (DictList_nil()) == NIL;
+axiom [DistListTag_cons_def]: forall k: Value, v: Value, d: DictList ::{DictList_cons(k,v,d)} DictList_tag (DictList_cons(k,v,d)) == CONS;
+// as a constructor for Dict
+function Dict_from_DicList (l : DictList) : Dict;
+function Dict_from_DicList_rev (l : DictList, acc: Dict) : Dict;
+axiom [Dict_from_DicList_rev_nil]: forall acc: Dict ::  Dict_from_DicList_rev(DictList_nil(), acc) == acc;
+axiom [Dict_from_DicList_rev_cons]: forall k: Value, v: Value, d: DictList, acc: Dict ::
+  Dict_from_DicList_rev(DictList_cons(k,v,d), acc) == Dict_from_DicList_rev(d,Dict_insert(acc, k, v));
+axiom [Dict_from_DicList_def]: forall dl: DictList:: {Dict_from_DicList(dl)}
+  Dict_from_DicList(dl) == Dict_from_DicList_rev(dl, Dict_empty());
+
+type AttributeNames;
+function AttributeNames_nil() : (AttributeNames);
+function AttributeNames_cons(x0 : string, x1 : AttributeNames) : (AttributeNames);
+function AttributeNames_tag (f: AttributeNames) : List_tag;
+function AttributeNames_contains (l : AttributeNames, x: string) : bool;
+function AttributeNames_len (l : AttributeNames) : int;
+function AttributeNames_index (l : AttributeNames, i : int) : string;
+function AttributeName_to_index (l : AttributeNames, f: string) : int;
+
+axiom [AttributeNames_len_nil_def]: AttributeNames_len (AttributeNames_nil()) == 0;
+axiom [AttributeNames_len_cons_def]: forall h : string, t : AttributeNames ::{AttributeNames_len (AttributeNames_cons(h,t))}
+  AttributeNames_len (AttributeNames_cons(h,t)) == 1 + AttributeNames_len(t);
+axiom [AttributeNames_tag_nil_def]: AttributeNames_tag(AttributeNames_nil()) == NIL;
+axiom [AttributeNames_tag_cons_def]: forall h : string, t : AttributeNames ::{} AttributeNames_tag (AttributeNames_cons(h,t)) == CONS;
+axiom [AttributeNames_contains_nil_def]: (forall x : string ::{AttributeNames_contains(AttributeNames_nil(), x)}
+  !AttributeNames_contains(AttributeNames_nil(), x));
+axiom [AttributeNames_contains_cons_def]: forall x : string, h : string, t : AttributeNames ::{AttributeNames_contains(AttributeNames_cons(h,t),x)}
+  AttributeNames_contains(AttributeNames_cons(h,t),x) == ((x==h) || AttributeNames_contains(t,x));
+axiom [AttributeNames_len_nonneg]: forall l: AttributeNames :: {AttributeNames_len(l)} AttributeNames_len(l) >= 0;
+axiom [AttributeNames_index_nil]: forall i : int ::{AttributeNames_index (AttributeNames_nil(), i)} (AttributeNames_index (AttributeNames_nil(), i)) == "";
+axiom [AttributeNames_index_zero]: forall h : string, t : AttributeNames ::{AttributeNames_index (AttributeNames_cons(h,t), 0)}
+  AttributeNames_index (AttributeNames_cons(h,t), 0) == h;
+axiom [AttributeNames_index_ind]: forall h : string, t : AttributeNames, i : int ::{AttributeNames_index (AttributeNames_cons(h,t), i)}
+  (i > 0) ==> (AttributeNames_index (AttributeNames_cons(h,t), i)) == AttributeNames_index (t, i - 1);
+axiom [AttributeNames_index_contains]: forall l: AttributeNames, i: int, x: string :: {AttributeNames_index(l,i), AttributeNames_contains(l,x)}
+  (AttributeNames_index(l,i) == x) ==> AttributeNames_contains(l,x);
+axiom [AttributeNames_index_ok]: forall l: AttributeNames, i: int:: {AttributeNames_index(l,i)}
+  ((AttributeNames_index(l,i)) != "") == (i < AttributeNames_len(l));
+axiom [AttributeName_to_index_nil_def]: forall f: string :: {AttributeName_to_index(AttributeNames_nil(), f)}
+  AttributeName_to_index(AttributeNames_nil(), f) == 0;
+axiom [AttributeName_to_index_cons_def_1]: forall h: string, t: AttributeNames :: {AttributeName_to_index(AttributeNames_cons(h,t), h)}
+  AttributeName_to_index(AttributeNames_cons(h,t), h) == 0;
+axiom [AttributeName_to_index_cons_def_2]: forall f: string, h: string, t: AttributeNames :: {AttributeName_to_index(AttributeNames_cons(h,t), f)}
+  !(h == f) ==> AttributeName_to_index(AttributeNames_cons(h,t), f) == AttributeName_to_index(t, f) + 1;
+
+function Class_mk (name: string, attributes: AttributeNames): Class;
+function Class_attributes (c: Class) : AttributeNames;
+function Class_name (c: Class): string;
+axiom [Class_attributes_def]: forall name: string, attributes: AttributeNames :: {Class_mk (name, attributes)}
+  Class_attributes(Class_mk (name, attributes)) == attributes;
+axiom [Class_name_def]: forall name: string, attributes: AttributeNames :: {Class_mk (name, attributes)}
+  Class_name(Class_mk (name, attributes)) == name;
+axiom [Class_eq_def]: forall c: Class, c': Class :: {c == c'}
+  (c == c') == (Class_name(c) == Class_name(c'));
+
+function Class_hasAttribute (c: Class, attribute: string): bool;
+axiom [Class_hasAttribute_def]: forall c: Class, attribute: string :: {Class_hasAttribute(c, attribute)}
+  Class_hasAttribute(c, attribute) == AttributeNames_contains(Class_attributes(c), attribute);
+
+function Class_err() : Class;
+axiom [Class_err_attributes_def]: Class_attributes(Class_err()) == AttributeNames_nil();
+
+function AttributeValues_empty (c: Class) : AttributeValues;
+axiom [AttributeValues_empty_def_valid]: forall c: Class, attribute: string :: {AttributeValues_empty(c)[attribute]}
+  Class_hasAttribute(c, attribute) ==> AttributeValues_empty(c)[attribute] == Value_none();
+axiom [AttributeValues_empty_def_invalid]: forall c: Class, attribute: string :: {AttributeValues_empty(c)[attribute]}
+  !Class_hasAttribute(c, attribute) ==> AttributeValues_empty(c)[attribute] == Value_exception(Error_message("Invalid Attribute of Class"));
+
+function AttributeValues_err () : AttributeValues;
+axiom [AttributeValues_err_def]: forall attribute: string :: {AttributeValues_err[attribute]}
+  AttributeValues_err()[attribute] == Value_exception(Error_message("Error ClassInstance"));
+
+function ClassInstance_mk (c: Class, av: AttributeValues) : ClassInstance;
+
+function ClassInstance_getAttributeValues (ci: ClassInstance) : AttributeValues;
+axiom [getAttributeValues_def]: forall c: Class, av: AttributeValues :: { ClassInstance_getAttributeValues(ClassInstance_mk (c, av))}
+  ClassInstance_getAttributeValues(ClassInstance_mk (c, av)) == av;
+
+function ClassInstance_getClass (ci: ClassInstance) : Class;
+axiom [get_Class_def]: forall c: Class, av: AttributeValues :: {ClassInstance_getClass(ClassInstance_mk (c, av))}
+  ClassInstance_getClass(ClassInstance_mk (c, av)) == c;
+
+axiom [TypeOf_class]: forall ci: ClassInstance :: {TypeOf(Value_class(ci))} TypeOf(Value_class(ci)) == ValueType_class(ClassInstance_getClass(ci));
+
+function ClassInstance_empty (c: Class) : ClassInstance;
+axiom [ClassInstance_mk_empty_get_attributevalues]: forall c: Class :: {ClassInstance_getAttributeValues(ClassInstance_empty (c))}
+  ClassInstance_getAttributeValues(ClassInstance_empty (c)) == AttributeValues_empty(c);
+axiom [ClassInstance_mk_empty_get_class]: forall c: Class :: {ClassInstance_getClass(ClassInstance_empty (c))}
+  ClassInstance_getClass(ClassInstance_empty (c)) == c;
+
+function ClassInstance_err (err: string) : ClassInstance;
+function ClassInstance_errortag (ci: ClassInstance): Error_tag;
+axiom [ClassInstance_err_tag]: forall err: string :: {ClassInstance_errortag(ClassInstance_err(err))}
+  ClassInstance_errortag(ClassInstance_err(err)) == ERR;
+axiom [ClassInstance_err_get_class_def]: forall err: string :: {ClassInstance_getClass(ClassInstance_err(err)) }
+  ClassInstance_getClass(ClassInstance_err(err)) == Class_err();
+axiom [ClassInstance_err_get_attributevalues_def]: forall err: string :: {ClassInstance_getAttributeValues(ClassInstance_err (err))}
+  ClassInstance_getAttributeValues(ClassInstance_err (err)) == AttributeValues_err();
+
+function ClassInstance_get_attribute(ci: ClassInstance, attribute: string) : Value;
+axiom [ClassInstance_get_attribute_def]: forall ci: ClassInstance, attribute: string ::{ClassInstance_get_attribute(ci, attribute)}
+  ClassInstance_get_attribute(ci, attribute) == ClassInstance_getAttributeValues(ci)[attribute];
+
+function ClassInstance_set_attribute (ci: ClassInstance, attribute: string, value: Value): ClassInstance;
+axiom [ClassInstance_set_attribute_def]: forall ci: ClassInstance, attribute: string, v: Value:: {ClassInstance_set_attribute(ci, attribute, v)}
+  ClassInstance_set_attribute(ci, attribute, v) == if Class_hasAttribute(ClassInstance_getClass(ci), attribute) then
+                                                      ClassInstance_mk(ClassInstance_getClass(ci), ClassInstance_getAttributeValues(ci)[attribute:=v])
+                                                  else ClassInstance_err("Set value for invalid");
+
+function get_ClassInstance (v: Value) : ClassInstance;
+axiom [get_ClassInstance_valid]: forall ci: ClassInstance :: {get_ClassInstance(Value_class(ci))}
+  get_ClassInstance(Value_class(ci)) == ci;
+axiom [get_ClassInstance_invalid]: forall v: Value :: {get_ClassInstance(v)}
+  !isClassInstance(v) ==> get_ClassInstance(v) == ClassInstance_err ("Not of Class type");
+
+function get_attribute(v: Value, attribute: string) : Value;
+axiom [get_attribute_def]: forall v: Value, attribute: string ::{get_attribute(v, attribute)}
+  get_attribute(v, attribute) == if isClassInstance(v) then
+                                    ClassInstance_get_attribute(get_ClassInstance(v), attribute)
+                                else Value_exception(Error_message("Not of Class type"));
+
+function set_attribute(v: Value, attribute: string, v': Value) : Value;
+axiom [set_attribute_def]: forall v: Value, attribute: string, v': Value ::{set_attribute(v, attribute, v')}
+  set_attribute(v, attribute, v') == if isClassInstance(v) then
+                                      Value_class(ClassInstance_set_attribute(get_ClassInstance(v), attribute, v'))
+                                    else Value_exception(Error_message("Not of Class type"));
+
+function get_Class (v: Value) : Class {
+  ClassInstance_getClass(get_ClassInstance (v))
+}
+
+function hasAttribute(v: Value, attribute: string): bool {
+  Class_hasAttribute (get_Class(v), attribute)
+}
+
+//Binary op function
+function int_to_real (i: int) : real;
+function str_repeat (s: string, i: int) : string;
+function Py_add (v1: Value, v2: Value) : Value;
+function Py_sub (v1: Value, v2: Value) : Value;
+function Py_mul (v1: Value, v2: Value) : Value;
+inline function bool_to_int (b: bool) : int {if b then 1 else 0}
+inline function bool_to_real (b: bool) : real {if b then 1.0 else 0.0}
+
+axiom [Py_add_ints]: forall i1: int, i2: int :: {Py_add(Value_int(i1), Value_int(i2))}
+  Py_add(Value_int(i1), Value_int(i2)) == Value_int(i1 + i2);
+axiom [Py_add_floats]: forall f1: real, f2: real :: {Py_add(Value_float(f1), Value_float(f2))}
+  Py_add(Value_float(f1), Value_float(f2)) == Value_float(f1 + f2);
+axiom [Py_add_bools]: forall b1: bool, b2: bool :: {Py_add(Value_bool(b1), Value_bool(b2))}
+  Py_add(Value_bool(b1), Value_bool(b2)) == Value_int(bool_to_int(b1) + bool_to_int(b2));
+axiom [Py_add_int_bool]: forall i: int, b: bool :: {Py_add(Value_int(i), Value_bool(b))}
+  Py_add(Value_int(i), Value_bool(b)) == Value_int(i + bool_to_int(b));
+axiom [Py_add_bool_int]: forall b: bool, i: int :: {Py_add(Value_bool(b), Value_int(i))}
+  Py_add(Value_bool(b), Value_int(i)) == Value_int(bool_to_int(b) + i);
+axiom [Py_add_int_float]: forall i: int, r: real :: {Py_add(Value_int(i), Value_float(r))}
+  Py_add(Value_int(i), Value_float(r)) == Value_float(r + int_to_real(i));
+axiom [Py_add_float_int]: forall r: real, i: int :: {Py_add(Value_float(r), Value_int(i))}
+  Py_add(Value_float(r), Value_int(i)) == Value_float(int_to_real(i) + r);
+axiom [Py_add_float_bool]: forall r: real, b: bool :: {Py_add(Value_float(r), Value_bool(b))}
+  Py_add(Value_float(r), Value_bool(b)) == Value_float(r + bool_to_real(b));
+axiom [Py_add_bool_float]: forall b: bool, r: real :: {Py_add(Value_bool(b), Value_float(r))}
+  Py_add(Value_bool(b), Value_float(r)) == Value_float(bool_to_real(b) + r);
+axiom [Py_add_strs]:forall s1: string, s2: string :: {Py_add(Value_str(s1), Value_str(s2))}
+  Py_add(Value_str(s1), Value_str(s2)) == Value_str(str.concat(s1, s2));
+axiom [Py_add_str_int]: forall s: string, i: int :: {Py_add(Value_str(s), Value_int(i))}
+  Py_add(Value_str(s), Value_int(i)) == Value_exception(Error_message("Cannot add string to int"));
+axiom [Py_add_int_str]: forall s: string, i: int :: {Py_add(Value_int(i), Value_str(s)) }
+  Py_add(Value_int(i), Value_str(s)) == Value_exception(Error_message("Cannot add string to int"));
+axiom [Py_add_str_bool]: forall s: string, b: bool :: {Py_add(Value_str(s), Value_bool(b))}
+  Py_add(Value_str(s), Value_bool(b)) == Value_exception(Error_message("Cannot add string to bool"));
+axiom [Py_add_bool_str]: forall s: string, b: bool :: {Py_add(Value_bool(b), Value_str(s))}
+  Py_add(Value_bool(b), Value_str(s)) == Value_exception(Error_message("Cannot add bool to string"));
+axiom [Py_add_unsupport]: forall v1: Value, v2: Value :: {Py_add(v1,v2)}
+  ((TypeOf(v1)!=BOOL && TypeOf(v1)!=INT && TypeOf(v1)!=FLOAT && TypeOf(v1)!=STR) ||
+  (TypeOf(v2)!=BOOL && TypeOf(v2)!=INT && TypeOf(v2)!=FLOAT && TypeOf(v2)!=STR)) ==>
+  Py_add(v1, v2) == Value_exception(Error_message("Operand Type is not supported"));
+
+axiom [Py_mul_ints]: forall i1: int, i2: int :: {Py_mul(Value_int(i1), Value_int(i2))}
+  Py_mul(Value_int(i1), Value_int(i2)) == Value_int(i1 * i2);
+axiom [Py_mul_bools]: forall b1: bool, b2: bool :: {Py_mul(Value_bool(b1), Value_bool(b2))}
+  Py_mul(Value_bool(b1), Value_bool(b2)) == Value_int(bool_to_int(b1) * bool_to_int(b2));
+axiom [Py_mul_int_bool]: forall i: int, b: bool :: {Py_mul(Value_int(i), Value_bool(b))}
+  Py_mul(Value_int(i), Value_bool(b)) == Value_int(i * bool_to_int(b));
+axiom [Py_mul_bool_int]: forall b: bool, i: int :: {Py_mul(Value_bool(b), Value_int(i))}
+  Py_mul(Value_bool(b), Value_int(i)) == Value_int(bool_to_int(b) * i);
+axiom [Py_mul_str]: forall s1: string, s2: string :: {Py_mul(Value_str(s1), Value_str(s2))}
+  Py_mul(Value_str(s1), Value_str(s2)) == Value_exception(Error_message("Cannot multiply two strings"));
+axiom [Py_mul_str_int]: forall s: string, i: int :: {Py_mul(Value_str(s), Value_int(i))}
+  Py_mul(Value_str(s), Value_int(i)) == Value_str(str_repeat(s, i));
+axiom [Py_mul_int_str]: forall s: string, i: int :: {Py_mul(Value_int(i), Value_str(s))}
+  Py_mul(Value_int(i), Value_str(s)) == Value_str(str_repeat(s, i));
+axiom [Py_mul_str_bool]: forall s: string, b: bool :: {Py_mul(Value_str(s), Value_bool(b))}
+  Py_mul(Value_str(s), Value_bool(b)) == Value_str(if b then s else "");
+axiom [Py_mul_bool_str]: forall s: string, b: bool :: {Py_mul(Value_bool(b), Value_str(s)) }
+  Py_mul(Value_bool(b), Value_str(s)) ==  Value_str(if b then s else "");
+axiom [Py_mul_unsupport]: forall v1: Value, v2: Value :: {Py_mul(v1,v2)}
+  ((TypeOf(v1)!=BOOL && TypeOf(v1)!=INT && TypeOf(v1)!=FLOAT && TypeOf(v1)!=STR) ||
+  (TypeOf(v2)!=BOOL && TypeOf(v2)!=INT && TypeOf(v2)!=FLOAT && TypeOf(v2)!=STR)) ==>
+  Py_mul(v1, v2) == Value_exception(Error_message("Operand Type is not supported"));
+
+
+//Testing
+
+procedure simple_add () returns () {
+  var x: Value, y: Value, z: Value, b: bool;
+  havoc b;
+  if (b) {
+    x := Value_int(1);
+  }
+  else {
+    x := Value_float(1.1);
+  }
+  y:= Py_add(x, Value_int(2));
+  assert [y_not_exception]: TypeOf(y)!= EXCEPTION;
+  assert [if_b_then_y_int]: b ==> TypeOf(y)== INT;
+  assert [x_y_same_type]: TypeOf(x) == TypeOf(y);
+  assert [y_is_instance_float]: isInstance(y,FLOAT);
+  assert [y_is_instance_int]: isInstance(y,INT);
+  z:= Py_add(x, Value_float(3.3));
+  assert [x_z_same_type]: TypeOf(x) == TypeOf(z);
+  assert [y_z_same_type]: (TypeOf(y) == TypeOf(z)) ==> !b;
+};
+
+procedure simple_add' (b: bool) returns (y: Value, z: Value)
+spec {
+  ensures [ens_y_not_exception]: TypeOf(y)!= EXCEPTION;
+  ensures [ens_if_b_then_y_int]: b ==> TypeOf(y)== INT;
+  ensures [ens_y_z_same_type]: TypeOf(y) == TypeOf(z);
+  ensures [ens_y_z_same_type']: (TypeOf(y) == TypeOf(z)) ==> !b;
+}
+{
+  var x: Value;
+  if (b) {
+    x := Value_int(1);
+  }
+  else {
+    x := Value_float(1.1);
+  }
+  y:= Py_add(x, Value_int(2));
+  z:= Py_add(x, Value_float(3.3));
+};
+
+#end
+
+#eval verify "cvc5" boogieTypePrelude
+
+def Boogie.prelude : Boogie.Program :=
+   Boogie.getProgram Strata.boogieTypePrelude |>.fst
+
+end Strata