@(subset_eq_trans … Ht2) -t2
@(subset_eq_trans … (lift_fsubst …))
[ <structure_append <structure_A_sn <structure_append <structure_L_sn
@(subset_eq_trans … Ht2) -t2
@(subset_eq_trans … (lift_fsubst …))
[ <structure_append <structure_A_sn <structure_append <structure_L_sn