-let rec A_rect (P: (A \to Type[0])) (f: (\forall (n: nat).(\forall (n0:
-nat).(P (ASort n n0))))) (f0: (\forall (a: A).((P a) \to (\forall (a0: A).((P
-a0) \to (P (AHead a a0))))))) (a: A) on a: P a \def match a with [(ASort n
-n0) \Rightarrow (f n n0) | (AHead a0 a1) \Rightarrow (f0 a0 ((A_rect P f f0)
-a0) a1 ((A_rect P f f0) a1))].
+implied let rec A_rect (P: (A \to Type[0])) (f: (\forall (n: nat).(\forall
+(n0: nat).(P (ASort n n0))))) (f0: (\forall (a: A).((P a) \to (\forall (a0:
+A).((P a0) \to (P (AHead a a0))))))) (a: A) on a: P a \def match a with
+[(ASort n n0) \Rightarrow (f n n0) | (AHead a0 a1) \Rightarrow (f0 a0
+((A_rect P f f0) a0) a1 ((A_rect P f f0) a1))].