theorem Cedar.Thm.compile_evaluate_extHasAttr {x₁ : Spec.Expr} {a : Spec.Attr} {l : List Spec.Attr} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} (heq : env ∼ εnv) (hwe : env.WellFormedFor (x₁.extHasAttr a l)) (hwε : εnv.WellFormedFor (x₁.extHasAttr a l)) (hok : SymCC.compile (x₁.extHasAttr a l) εnv = Except.ok t) (ih : CompileEvaluate x₁) : Spec.evaluate (x₁.extHasAttr a l) env.request env.entities ∼ t

theorem Cedar.Thm.compile_interpret_extHasAttr {x₁ : Spec.Expr} {a : Spec.Attr} {l : List Spec.Attr} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} {t : SymCC.Term} (hI : I.WellFormed εnv.entities) (hwε : εnv.WellFormedFor (x₁.extHasAttr a l)) (hok : SymCC.compile (x₁.extHasAttr a l) εnv = Except.ok t) (ih : CompileInterpret x₁) : SymCC.compile (x₁.extHasAttr a l) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)