-#L1 #L2 @(f2_ind ?? length2 ?? L1 L2) -L1 -L2
-#x #IH * [2: #L1 #I1 ] * [2,4: #L2 #I2 ]
-[ cases I1 -I1 [ * | #I1 #V1 ] cases I2 -I2 [1,3: * |*: #I2 #V2 ] ]
-#Hx #n1 #n2 #Hn #m1 #m2 #Hm destruct
-[ elim (lveq_fwd_void_void … Hn) * #x #H destruct
- elim (lveq_fwd_void_void … Hm) * #y #H destruct
- [ lapply (lveq_inv_void_succ_sn … Hn) -Hn #Hn
- lapply (lveq_inv_void_succ_sn … Hm) -Hm #Hm
- elim (IH … Hn … Hm) -IH -Hn -Hm // #H1 #H2 destruct
- /2 width=1 by conj/
- | elim (lveq_fwd_inj_succ_sn … Hn … Hm) * #z #H destruct
- [ lapply (lveq_inv_void_succ_dx … Hn) -Hn #Hn
- lapply (lveq_inv_void_succ_dx … Hm) -Hm #Hm
- elim (IH … Hn … Hm) -IH -Hn -Hm [2: normalize // ] #H1 #H2 destruct (**) (* avoid normalize *)
- /2 width=1 by conj/
- | lapply (lveq_inv_void_succ_sn … Hn) -Hn #Hn
- lapply (lveq_inv_void_succ_sn … Hm) -Hm #Hm
- elim (IH … Hn … Hm) -IH -Hn -Hm // #H1 #H2 destruct
- /2 width=1 by conj/
- ]
- | elim (lveq_fwd_inj_succ_dx … Hn … Hm) * #z #H destruct
- [ lapply (lveq_inv_void_succ_sn … Hn) -Hn #Hn
- lapply (lveq_inv_void_succ_sn … Hm) -Hm #Hm
- elim (IH … Hn … Hm) -IH -Hn -Hm // #H1 #H2 destruct
- /2 width=1 by conj/
- | lapply (lveq_inv_void_succ_dx … Hn) -Hn #Hn
- lapply (lveq_inv_void_succ_dx … Hm) -Hm #Hm
- elim (IH … Hn … Hm) -IH -Hn -Hm [2: normalize // ] #H1 #H2 destruct (**) (* avoid normalize *)
- /2 width=1 by conj/
- ]
- | lapply (lveq_inv_void_succ_dx … Hn) -Hn #Hn
- lapply (lveq_inv_void_succ_dx … Hm) -Hm #Hm
- elim (IH … Hn … Hm) -IH -Hn -Hm [2: normalize // ] #H1 #H2 destruct (**) (* avoid normalize *)
- /2 width=1 by conj/
- ]
-| lapply (lveq_fwd_abst_bind_length_le … Hn) #HL
- elim (le_to_or_lt_eq … HL) -HL #HL
- [ elim (lveq_inv_void_dx_length … Hn) -Hn // #x1 #Hn #H #_ destruct
- elim (lveq_inv_void_dx_length … Hm) -Hm // #y1 #Hm #H #_ destruct
- elim (IH … Hn … Hm) -IH -Hn -Hm -HL [2: normalize // ] #H1 #H2 destruct (**) (* avoid normalize *)
- /2 width=1 by conj/
- | elim (lveq_eq_ex … HL) -HL #x #HL
- elim (lveq_inv_pair_sn … HL … Hn) -Hn #H1 #H2 destruct
- elim (lveq_inv_pair_sn … HL … Hm) -Hm #H1 #H2 destruct
- /2 width=1 by conj/
- ]
-| lapply (lveq_fwd_bind_abst_length_le … Hn) #HL
- elim (le_to_or_lt_eq … HL) -HL #HL
- [ elim (lveq_inv_void_sn_length … Hn) -Hn // #x1 #Hn #H #_ destruct
- elim (lveq_inv_void_sn_length … Hm) -Hm // #y1 #Hm #H #_ destruct
- elim (IH … Hn … Hm) -IH -Hn -Hm -HL // #H1 #H2 destruct
- /2 width=1 by conj/
- | lapply (sym_eq ??? HL) -HL #HL
- elim (lveq_eq_ex … HL) -HL #x #HL
- elim (lveq_inv_pair_dx … HL … Hn) -Hn #H1 #H2 destruct
- elim (lveq_inv_pair_dx … HL … Hm) -Hm #H1 #H2 destruct
- /2 width=1 by conj/
- ]
-| elim (lveq_inv_pair_pair… Hn) -Hn #x #_ #H1 #H2 destruct
- elim (lveq_inv_pair_pair… Hm) -Hm #y #_ #H1 #H2 destruct
- /2 width=1 by conj/
-| elim (lveq_inv_atom_bind … Hn) -Hn #x #Hn #H1 #H2 destruct
- elim (lveq_inv_atom_bind … Hm) -Hm #y #Hm #H1 #H2 destruct
- elim (IH … Hn … Hm) -IH -Hn -Hm /2 width=1 by conj/
-| elim (lveq_inv_bind_atom … Hn) -Hn #x #Hn #H1 #H2 destruct
- elim (lveq_inv_bind_atom … Hm) -Hm #y #Hm #H1 #H2 destruct
- elim (IH … Hn … Hm) -IH -Hn -Hm /2 width=1 by conj/
-| elim (lveq_inv_atom_atom … Hn) -Hn #H1 #H2 destruct
- elim (lveq_inv_atom_atom … Hm) -Hm #H1 #H2 destruct
- /2 width=1 by conj/
-]