Opt compile correctness

theorem Opt.compile.correctness (x : Expr) (εnv : SymEnv) :  Opt.compile x εnv = (do    let term ← SymCC.compile x εnv    let footprint := footprint x εnv    .ok { term, footprint }  ):= by  cases x  case lit p => exact Opt.compile.correctness.lit p εnv  case var v => exact Opt.compile.correctness.var v εnv  case and x₁ x₂ | or x₁ x₂ =>    first    | exact (Opt.compile.correctness.andor x₁ x₂ εnv).left    | exact (Opt.compile.correctness.andor x₁ x₂ εnv).right  case ite x₁ x₂ x₃       => exact Opt.compile.correctness.ite x₁ x₂ x₃ εnv  case unaryApp op x₁     => exact Opt.compile.correctness.unaryApp op x₁ εnv  case binaryApp op x₁ x₂ => exact Opt.compile.correctness.binaryApp op x₁ x₂ εnv  case getAttr x₁ attr    => exact Opt.compile.correctness.getAttr x₁ attr εnv  case hasAttr x₁ attr    => exact Opt.compile.correctness.hasAttr x₁ attr εnv  case set xs             => exact Opt.compile.correctness.set xs εnv  case record m           => exact Opt.compile.correctness.record m εnv  case call xfn args      => exact Opt.compile.correctness.call xfn args εnv