-inductive conv : T →T → Prop ≝
- | cbeta: ∀P,M,N. conv (App (Lambda P M) N) (M[0 ≝ N])
- | cappl: ∀M,M1,N. conv M M1 → conv (App M N) (App M1 N)
- | cappr: ∀M,N,N1. conv N N1 → conv (App M N) (App M N1)
- | claml: ∀M,M1,N. conv M M1 → conv (Lambda M N) (Lambda M1 N)
- | clamr: ∀M,N,N1. conv N N1 → conv (Lambda M N) (Lambda M N1)
- | cprodl: ∀M,M1,N. conv M M1 → conv (Prod M N) (Prod M1 N)
- | cprodr: ∀M,N,N1. conv N N1 → conv (Prod M N) (Prod M N1)
- | cd: ∀M,M1. conv (D M) (D M1).
+inductive conv1 : T →T → Prop ≝
+ | cbeta: ∀P,M,N. conv1 (App (Lambda P M) N) (M[0 ≝ N])
+ | cappl: ∀M,M1,N. conv1 M M1 → conv1 (App M N) (App M1 N)
+ | cappr: ∀M,N,N1. conv1 N N1 → conv1 (App M N) (App M N1)
+ | claml: ∀M,M1,N. conv1 M M1 → conv1 (Lambda M N) (Lambda M1 N)
+ | clamr: ∀M,N,N1. conv1 N N1 → conv1 (Lambda M N) (Lambda M N1)
+ | cprodl: ∀M,M1,N. conv1 M M1 → conv1 (Prod M N) (Prod M1 N)
+ | cprodr: ∀M,N,N1. conv1 N N1 → conv1 (Prod M N) (Prod M N1)
+ | cd: ∀M,M1. conv1 (D M) (D M1).