Compile is complete

theorem compile_is_complete {x : Expr} {εnv : SymEnv} {t : Term.Outcome εnv} {o : Outcome Value} :  εnv.WellFormedFor x →  compile x εnv = .ok t →  o ∈ₒ t →  ∃ (env : Env),    env.WellFormedFor x ∧    env ∈ᵢ εnv ∧    evaluate x env.request env.entities ∼ o:= by  intros h₁ h₂ h₃  replace ⟨I, h₃, h₅⟩ := h₃  have ⟨env, h₆, h₇⟩ := exists_wf_env h₁ h₃  exists env  simp only [h₇, true_and]  constructor  · exists I  · have ⟨o', h₈, h₉⟩ := same_results_implies_exists_outcome (compile_bisimulation h₁ h₇ h₃ h₆ h₂)    have h₁₀ := same_outcomes_implies_eq h₅ h₉    subst h₁₀    exact h₈