- | p2: \forall i,j. T i \to P j \to P (i + j)
-with T: nat \to Prop \def
- | t1: \forall i. P i \to T (i * 3)
- | t2: \forall i. T i \to T (i * 3)
+ | p2: ∀i,j. T i → P j → P (i + j)
+with T: nat → Prop ≝
+ | t1: ∀i. P i → T (i * 3)
+ | t2: ∀i. T i → T (i * 3)