- lapply (fle_fwd_pair_sn … H2T) -H2T #H2T
- lapply (fle_fwd_pair_sn … H3T) -H3T #H3T
- @and3_intro[ /3 width=5 by fle_flat, fle_bind/ ] (**) (* full auto too slow *)
- @fle_bind_sn_ge //
- [1,3: /3 width=1 by fle_flat_dx_dx, fle_bind_dx_sn/
- |2,4: /4 width=3 by fle_flat_sn, fle_flat_dx_sn, fle_flat_dx_dx, fle_shift, fle_lifts_sn/
+ lapply (fsle_fwd_pair_sn … H2T) -H2T #H2T
+ lapply (fsle_fwd_pair_sn … H3T) -H3T #H3T
+ @and3_intro[ /3 width=5 by fsle_flat, fsle_bind/ ] (**) (* full auto too slow *)
+ @fsle_bind_sn_ge //
+ [1,3: /3 width=1 by fsle_flat_dx_dx, fsle_bind_dx_sn/
+ |2,4: /4 width=3 by fsle_flat_sn, fsle_flat_dx_sn, fsle_flat_dx_dx, fsle_shift, fsle_lifts_sn/