Holist RegisterTheorem/ApplyTactic sequence that proves `|- p => q`

proof.log

# Register `p=T |- p=T`
> RegisterTheoremRequest {
  theorem {
    hypotheses: "(a (a (c (fun (bool) (fun (bool) (bool))) =) (v (bool) p)) (c (bool) T))"
    conclusion: "(a (a (c (fun (bool) (fun (bool) (bool))) =) (v (bool) p)) (c (bool) T))"
    tag: THEOREM
    fingerprint: 4307889383570985746
  }
} 
< RegisterTheoremResponse {
  fingerprint: 4307889383570985746
}

# On g0: `|- p => q`, apply SUBST1_TAC `p=T |- p=T`
> ApplyTacticRequest {
  goal {
    conclusion: "(a (a (c (fun (bool) (fun (bool) (bool))) ==>) (v (bool) p)) (v (bool) q))"
    tag: THEOREM
  }
  tactic: "SUBST1_TAC THM 4307889383570985746"
}
# We receive g1: `|- T => q` which is erroneous (and should have failed as the theorem argument hypotheses are not in the goal's hypotheses).
< ApplyTacticResponse {
  goals {
    goals {
      conclusion: "(a (a (c (fun (bool) (fun (bool) (bool))) ==>) (c (bool) T)) (v (bool) q))"
      tag: GOAL
      pretty_printed: "\n`T ==> q`\n"
    }
  }
}

# Register `q=T |- q=T`
> RegisterTheoremRequest {
  theorem {
    hypotheses: "(a (a (c (fun (bool) (fun (bool) (bool))) =) (v (bool) q)) (c (bool) T))"
    conclusion: "(a (a (c (fun (bool) (fun (bool) (bool))) =) (v (bool) q)) (c (bool) T))"
    tag: THEOREM
    fingerprint: 2325052827426937061
  }
}
< RegisterTheoremResponse {
  fingerprint: 2325052827426937061
}

# Apply SUBST1_TAC `q=T |- q=T` on g1
> ApplyTacticRequest {
  goal {
    conclusion: "(a (a (c (fun (bool) (fun (bool) (bool))) ==>) (c (bool) T)) (v (bool) q))"
    tag: THEOREM
  }
  tactic: "SUBST1_TAC THM 2325052827426937061"
}
# We receive g2: `|- T => T`
< ApplyTacticResponse {
  goals {
    goals {
      conclusion: "(a (a (c (fun (bool) (fun (bool) (bool))) ==>) (c (bool) T)) (c (bool) T))"
      tag: GOAL
      pretty_printed: "\n`T ==> T`\n"
    }
  }
}

# Finish the proof with an ITAUT on g2
> ApplyTacticRequest {
  goal {
    conclusion: "(a (a (c (fun (bool) (fun (bool) (bool))) ==>) (c (bool) T)) (c (bool) T))"
    tag: THEOREM
  }
  tactic: "ITAUT_TAC"
}
# There is no remaining goals
< ApplyTacticResponse {
  goals {
  }
}