- updated equivalence on referred entries: it nust be degree-based

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / frees / frees.etc

(* A Basic_A2 lemma we do not need so far *)
axiom frees_pair_flat: ∀L,T,f1,I1,V1. L.ⓑ{I1}V1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
                       ∀f2,I2,V2. L.ⓑ{I2}V2 ⊢ 𝐅*⦃T⦄ ≡ f2 →
                       ∀f0. f1 ⋓ f2 ≡ f0 →
                       ∀I0,I. L.ⓑ{I0}ⓕ{I}V1.V2 ⊢ 𝐅*⦃T⦄ ≡ f0.