+(*definition cast ≝ λA,B:CProp.λa:A.a.*)
+axiom cast: ∀A,B:CProp.B → A.
+
+(*notation < "\infrule (t\atop ⋮) (b \ALPOSTODI a) (? \ERROR)" with precedence 19
+for @{ 'caste $a $b $t }.
+interpretation "cast" 'caste a b t = (cast a b t).*)
+notation < "\infrule (t\atop ⋮) mstyle color #ff0000 (b) (? \ERROR)" with precedence 19
+for @{ 'caste $a $b $t }.
+interpretation "cast" 'caste a b t = (cast a b t).