matita/matita/contribs/lambdadelta/basic_2/etc_new/frees/frees.etc

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