Well Typed Policy ok implies exists typed exprs

theorem wellTypedPolicy_ok_implies_exists_typed_exprs  {Γ : TypeEnv} {p p' : Policy}  (hwt : wellTypedPolicy p Γ = .ok p') :  ∃ tx tx' : TypedExpr, ∃ c,    TypedExpr.WellTyped Γ tx.liftBoolTypes ∧    TypedExpr.WellTyped Γ tx' ∧    typeOf (substituteAction Γ.reqty.action p.toExpr) ∅ Γ = Except.ok (tx, c) ∧    p'.toExpr = tx'.toExpr ∧    tx' =      (TypedExpr.and (TypedExpr.lit (Prim.bool true) (.bool .anyBool))      (TypedExpr.and (TypedExpr.lit (Prim.bool true) (.bool .anyBool))      (TypedExpr.and (TypedExpr.lit (Prim.bool true) (.bool .anyBool))        tx.liftBoolTypes      (.bool .anyBool))      (.bool .anyBool))      (.bool .anyBool)) ∧    tx.liftBoolTypes.typeOf = .bool .anyBool:= by  simp only [wellTypedPolicy, bind, Except.bind] at hwt  split at hwt  contradiction  rename_i tx hwt  simp only [Except.ok.injEq] at hwt ; subst p'  simp only [typecheckPolicy] at hwt  split at hwt  · rename_i tx' c hty    split at hwt    · rename_i hwt_bool      have hwf_lift := typechecked_is_well_typed_after_lifting hty      simp only [Except.ok.injEq] at hwt ; subst tx'      have :        tx.liftBoolTypes.typeOf = .bool .anyBool      := by        have := lifted_type_is_top hwt_bool        simp only [←type_of_after_lifted_is_lifted] at this        simp only [this, CedarType.liftBoolTypes, BoolType.lift]      -- Construct a `TypedExpr` for the condition      -- TODO: this has likely been done somewhere else?      generalize htx'' :        (TypedExpr.and (TypedExpr.lit (Prim.bool true) (.bool .anyBool))        (TypedExpr.and (TypedExpr.lit (Prim.bool true) (.bool .anyBool))        (TypedExpr.and (TypedExpr.lit (Prim.bool true) (.bool .anyBool))          tx.liftBoolTypes        (.bool .anyBool))        (.bool .anyBool))        (.bool .anyBool)) = tx''      have hwf_tx'' : TypedExpr.WellTyped Γ tx'' := by        simp only [←htx'']        constructor        · repeat constructor        · constructor          · repeat constructor          · constructor            · repeat constructor            · exact hwf_lift            · repeat constructor            · exact this          · rfl          · rfl        · rfl        · rfl      exists tx, tx'', c      simp only [        hwf_lift, hwf_tx'', hty, htx'', this,        true_and, and_true,      ]      simp only [        Policy.toExpr,        Scope.toExpr,        PrincipalScope.toExpr,        ActionScope.toExpr,        ResourceScope.toExpr,        Conditions.toExpr,        Condition.toExpr,        List.foldl,        List.reverse,        List.reverseAux,        TypedExpr.toExpr,        ←htx'',        type_lifting_preserves_expr tx,      ]    · contradiction  · contradiction