- rename σ₁ into a.
- rename σ₂ into b.
- rewrite mapOptionTree_distributes.
- rewrite mapOptionTree_distributes.
- set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₁)) as A.
- set (take_lev (ec :: lev) Σ₁) as A'.
- set (mapOptionTree (garrowfy_leveled_code_types (S n)) (drop_lev (ec :: lev) Σ₂)) as B.
- set (take_lev (ec :: lev) Σ₂) as B'.