(* Basic_2A1: uses: fpbq_ind_alt *)
lemma fpb_inv_fpbc:
- â\88\80G1,G2,L1,L2,T1,T2. â\9dªG1,L1,T1â\9d« â\89½ â\9dªG2,L2,T2â\9d« →
- â\88¨â\88¨ â\9dªG1,L1,T1â\9d« â\89\85 â\9dªG2,L2,T2â\9d«
- | â\9dªG1,L1,T1â\9d« â\89» â\9dªG2,L2,T2â\9d«.
+ â\88\80G1,G2,L1,L2,T1,T2. â\9d¨G1,L1,T1â\9d© â\89½ â\9d¨G2,L2,T2â\9d© →
+ â\88¨â\88¨ â\9d¨G1,L1,T1â\9d© â\89\85 â\9d¨G2,L2,T2â\9d©
+ | â\9d¨G1,L1,T1â\9d© â\89» â\9d¨G2,L2,T2â\9d©.
#G1 #G2 #L1 #L2 #T1 #T2 #H
elim (feqx_dec G1 G2 L1 L2 T1 T2)
/4 width=1 by fpbc_intro, or_intror, or_introl/