(* Basic properties *********************************************************)
-lemma applv_nil: â\88\80T. â\92¶â\97\8a.T = T.
+lemma applv_nil: â\88\80T. â\92¶â\92º.T = T.
// qed.
-lemma applv_cons: ∀V,Vs,T. ⒶV@Vs.T = ⓐV.ⒶVs.T.
+lemma applv_cons: ∀V,Vs,T. ⒶV⨮Vs.T = ⓐV.ⒶVs.T.
// qed.
(* Properties with simple terms *********************************************)