diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean
index baa0878..a0345a5 100644
--- a/verification/Proofs/AxiomCheck.lean
+++ b/verification/Proofs/AxiomCheck.lean
@@ -41,3 +41,23 @@ import Proofs.PinStore
 #print axioms LTLAcc.pin_prefix_correct
 #print axioms LTLAcc.fork_distinct
 #print axioms LTLAcc.pin_prefix_nonvacuous
+
+#print axioms LTLAcc.MTH_single
+#print axioms LTLAcc.MTH_split
+#print axioms LTLAcc.Root_left
+#print axioms LTLAcc.Root_one
+#print axioms LTLAcc.Root_one_cons
+#print axioms LTLAcc.Root_right
+#print axioms LTLAcc.acceptCons
+#print axioms LTLAcc.eq_dropLast_append_of_getLast?
+#print axioms LTLAcc.exists_singleton_of_length_one
+#print axioms LTLAcc.getD_drop
+#print axioms LTLAcc.getD_take
+#print axioms LTLAcc.hleaf
+#print axioms LTLAcc.hnode
+#print axioms LTLAcc.kbelow
+#print axioms LTLAcc.kbelow_eq_of_pow2_between
+#print axioms LTLAcc.pinAccept
+#print axioms LTLAcc.pinExtract
+#print axioms LTLAcc.pow2_exp_unique
+#print axioms LTLAcc.take_append_drop
diff --git a/verification/check.sh b/verification/check.sh
index dd7ec7f..8e1a5e6 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -55,6 +55,25 @@ declare -A CONES=(
   [LTLAcc.pin_prefix_correct]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
   [LTLAcc.fork_distinct]="propext, LTLAcc.sha256, Quot.sound"
   [LTLAcc.pin_prefix_nonvacuous]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.MTH_single]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.MTH_split]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.Root_left]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.Root_one]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.Root_one_cons]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.Root_right]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.acceptCons]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.exists_singleton_of_length_one]="propext, Classical.choice, Quot.sound"
+  [LTLAcc.getD_drop]="propext, Quot.sound"
+  [LTLAcc.getD_take]="propext, Quot.sound"
+  [LTLAcc.hleaf]="LTLAcc.sha256"
+  [LTLAcc.hnode]="LTLAcc.sha256"
+  [LTLAcc.kbelow]="propext, Quot.sound"
+  [LTLAcc.kbelow_eq_of_pow2_between]="propext, Quot.sound"
+  [LTLAcc.pinAccept]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.pinExtract]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.pow2_exp_unique]="propext, Quot.sound"
+  [LTLAcc.take_append_drop]=""
+  [LTLAcc.eq_dropLast_append_of_getLast?]="propext"
 )
 
 free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'