(* Properties with simple terms *********************************************)
lemma tweq_simple_trans:
- â\88\80T1,T2. T1 â\89\85 T2 â\86\92 ð\9d\90\92â¦\83T1â¦\84 â\86\92 ð\9d\90\92â¦\83T2â¦\84.
+ â\88\80T1,T2. T1 â\89\85 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)