-fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ÷ A → L = L1 → T = T1 →
- ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → L2 ⊢ T2 ÷ A.
+fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T1 →
+ ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A.
-lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ➡ L2 →
- ∀T2. T1 ➡ T2 → L2 ⊢ T2 ÷ A.
+lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ➡ L2 →
+ ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A.