frozen_nominal.md

Key : Type;
Frozen : {
  @Frozen : (A : Type, k : Key) -> Type;
  freeze : {A} -> (k : Key, x : A) -> Frozen(A, k);
  unfreeze : {A} -> (k : Key, x : Frozen(A, k)) -> A;
};

Nat_TE = ($Nat_key) => {
  // Nat.te
  @Nat = Frozen($Nat_key, Int);
  zero = Frozen.freeze($Nat_key, Int.zero);
  one = Frozen.freeze($Nat_key, Int.one);
  add = (n, m) => {
    n = Frozen.unfreeze($Nat_key, n);
    m = Frozen.unfreeze($Nat_key, m);
    Int.add(n, m)
  };
}
Nat_TEI = {
  // Nat.tei
  @Nat : Type;
  zero : @Nat;
  one : @Nat;
  add : (n : @Nat, m : @Nat) -> 
};
M_TE = ($Nat_key, $M_key) => {
  Nat : Nat_TEI = Nat_TE($Nat_key);
  // M.te
  // this will fail
  one : Int = Nat.one;
};