theorem para_diamond (t t1 : Trm) : para t t1 → ∀ (t2 : Trm), para t t2 → ∃ (t' : Trm), para t1 t' ∧ para t2 t'

theorem multi_para_diamond_core (t t1 t2 : Trm) : para t t1 ∧ multi_para t t2 → ∃ (t' : Trm), multi_para t1 t' ∧ para t2 t'

theorem multi_para_diamond (t t1 t2 : Trm) : multi_para t t1 ∧ multi_para t t2 → ∃ (t' : Trm), multi_para t1 t' ∧ multi_para t2 t'

theorem beta_red_confluence (t t1 t2 : Trm) : multi_red t t1 ∧ multi_red t t2 → ∃ (t' : Trm), multi_red t1 t' ∧ multi_red t2 t'