Of Record Type preserves attr

theorem ofRecordType_preserves_attr  {rty : RecordType} {attr : Attr} {qty : Qualified CedarType} {ty : CedarType}  (hattr_exists : Data.Map.find? rty attr = some qty)  (hattr_ty : qty.getType = ty) :  ∃ attr_ty : TermType,    (Data.Map.mk (TermType.ofRecordType rty.1)).find? attr = some attr_ty ∧    match attr_ty with    | .option attr_ty' => TermType.ofType ty = attr_ty' ∧ ¬qty.isRequired    | _ => TermType.ofType ty = attr_ty ∧ qty.isRequired:= by  cases rty with | mk rty_1 =>  induction rty_1  case nil => simp [Data.Map.find?] at hattr_exists  case cons head tail ih =>    have ⟨k, v⟩ := head    simp only [Data.Map.find?, List.find?, TermType.ofRecordType, Data.Map.toList_mk_id, Bool.not_eq_true]    simp only [Data.Map.find?, List.find?, Data.Map.toList_mk_id, Bool.not_eq_true] at hattr_exists ih    cases e : k == attr    case false =>      simp only [e] at ⊢ hattr_exists      apply ih hattr_exists    case true =>      simp only [e, Option.some.injEq] at hattr_exists      simp only [hattr_exists, Option.some.injEq, exists_eq_left']      cases qty with      | optional =>        simp only [TermType.ofQualifiedType, Qualified.isRequired, and_true]        simp only [Qualified.getType] at hattr_ty        simp [hattr_ty]      | required =>        simp only [          TermType.ofQualifiedType, Qualified.isRequired,          Bool.true_eq_false, and_false, and_true,        ]        simp only [Qualified.getType] at hattr_ty        simp only [hattr_ty]        -- TermType.ofType never produces an option type        unfold TermType.ofType        split        case h_1 hof_type =>          split at hof_type          all_goals contradiction        simp