+ncoercion foo : ∀_l:list T. list S ≝ c
+ on _l : list T
+ to list ?.
+
+naxiom P : list S → Prop.
+
+ndefinition t1 ≝ ∀x:list T.P x → ?. ##[ napply Prop; ##] nqed.
+
+ncoercion bar : ∀_l:list T. S → S ≝ λ_.λx.x
+ on _l : list T
+ to Π_.?.
+
+naxiom Q : (S → S) → Prop.