(* Properties with simple terms *********************************************)
lemma teqw_simple_trans:
- â\88\80T1,T2. T1 â\89\83 T2 â\86\92 ð\9d\90\92â\9dªT1â\9d« â\86\92 ð\9d\90\92â\9dªT2â\9d«.
+ â\88\80T1,T2. T1 â\89\83 T2 â\86\92 ð\9d\90\92â\9d¨T1â\9d© â\86\92 ð\9d\90\92â\9d¨T2â\9d©.
#T1 #T2 * -T1 -T2
[4,5: #p #V1 #V2 #T1 #T2 [ #_ ] #H
elim (simple_inv_bind … H)