This file proves the compilation lemmas for .unaryApp expressions.

theorem Cedar.Thm.compile_evaluate_unaryApp {op₁ : Spec.UnaryOp} {x₁ : Spec.Expr} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} (heq : env ∼ εnv) (hwe : env.WellFormedFor (Spec.Expr.unaryApp op₁ x₁)) (hwε : εnv.WellFormedFor (Spec.Expr.unaryApp op₁ x₁)) (hok : SymCC.compile (Spec.Expr.unaryApp op₁ x₁) εnv = Except.ok t) (ih : CompileEvaluate x₁) : Spec.evaluate (Spec.Expr.unaryApp op₁ x₁) env.request env.entities ∼ t

theorem Cedar.Thm.interpret_compileApp₁ {op₁ : Spec.UnaryOp} {t t₁ : SymCC.Term} {εs : SymCC.SymEntities} {I : SymCC.Interpretation} (hI : I.WellFormed εs) (hwt : SymCC.Term.WellFormed εs t₁) (hok : SymCC.compileApp₁ op₁ t₁ = Except.ok t) : SymCC.compileApp₁ op₁ (SymCC.Term.interpret I t₁) = Except.ok (SymCC.Term.interpret I t)

theorem Cedar.Thm.compile_interpret_unaryApp {op₁ : Spec.UnaryOp} {x₁ : Spec.Expr} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} {t : SymCC.Term} (hI : I.WellFormed εnv.entities) (hwε : εnv.WellFormedFor (Spec.Expr.unaryApp op₁ x₁)) (hok : SymCC.compile (Spec.Expr.unaryApp op₁ x₁) εnv = Except.ok t) (ih : CompileInterpret x₁) : SymCC.compile (Spec.Expr.unaryApp op₁ x₁) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)