[Elab.step] ✅️ expected type: Prop, term
    True
  [Elab.step.result] True
[Elab.step] ✅️ expected type: True, term
    by
      skip
      trivial
  [Elab.step.result] ?m
[Elab.step] ✅️ 
      skip
      trivial
  [Elab.step] ✅️ 
        skip
        trivial
    [Elab.step] ✅️ skip
    [Elab.step] ✅️ trivial
      [Elab.step] 💥️ (apply And.intro✝) <;> trivial
        [Elab.step] 💥️ focus
              apply And.intro✝
              with_annotate_state"<;>" skip
              all_goals trivial
          [Elab.step] 💥️ 
                apply And.intro✝
                with_annotate_state"<;>" skip
                all_goals trivial
            [Elab.step] 💥️ 
                  apply And.intro✝
                  with_annotate_state"<;>" skip
                  all_goals trivial
              [Elab.step] 💥️ apply And.intro✝
      [Elab.step] ✅️ apply True.intro✝