(* *)
(**************************************************************************)
-include "lambda/ext.ma".
-
+include "pts_dummy/ext.ma".
+(*
(* ARITIES ********************************************************************)
(* An arity is a normal term representing the functional structure of a term.
∀i. nth i ? E1 sort ≅ nth i ? E2 sort.
#E1 #E2 #H #i @(all2_nth … aeq) //
qed.
+*)