prove type_safe

[github-actions]

tibi/Tibi/Props/Typing.lean

Line 71 in 58ea612

-- TODO prove type_safe

      else
        isFalse fun ht => heq (HasType.det ht ht')
  | .unknown => isFalse (Expr.typeCheck_complete h)
-/

-- TODO prove type_safe
/-
theorem type_safe {e : Expr ctx ty}
: HasType e t → Eval e r → ∃ v, r = .ok v
| .Int64 hLt hGe, .Const ..      => ⟨Int64.mk ⟨_, hLt, hGe⟩, rfl⟩