Skip to content

Extract "Boehm_construction" from the proof of subtree_equiv_lemma#1381

Open
binghe wants to merge 2 commits intoHOL-Theorem-Prover:developfrom binghe:Boehm_construction