The downloadable PDFs of all IA-32 Architectures Software Developer's Manual volumes are at version 086.
2025-01-14 (Tue)
#1 forall {m n : nat} (H : m.+1 = n.+1), f_equal succn (f_equal predn H) = H を証明する
昨日の my_vector_caseS で Hn を noconf_nat_inv Hn noconf_nat に置き換えるのに
noconf_natK という補題を使った。
そのために no con