(* Properties with simple terms *********************************************)
-lemma applv_simple: â\88\80T,Vs. ð\9d\90\92â\9dªTâ\9d« â\86\92 ð\9d\90\92â\9dªâ\92¶Vs.Tâ\9d«.
+lemma applv_simple: â\88\80T,Vs. ð\9d\90\92â\9d¨Tâ\9d© â\86\92 ð\9d\90\92â\9d¨â\92¶Vs.Tâ\9d©.
#T * //
qed.