matita/matita/contribs/lambdadelta/basic_2/etc/fqu/fquq.etc

   1 (* Removed theorems *********************************************************)
   2
   3 lemma fquqa_drop: ∀G,L,K,T,U,k.
   4                   ⬇[k] L ≡ K → ⬆[0, k] T ≡ U → ⦃G, L, U⦄ ⊐⊐⸮ ⦃G, K, T⦄.
   5 #G #L #K #T #U #k @(ynat_ind … k) -k /3 width=3 by fqu_drop, or_introl/
   6 #HLK #HTU >(drop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T //
   7 qed.
   8
   9 inductive fquq: tri_relation genv lenv term ≝
  10 | fquq_lref_O : ∀I,G,L,V. fquq G (L.ⓑ{I}V) (#0) G L V
  11 | fquq_pair_sn: ∀I,G,L,V,T. fquq G L (②{I}V.T) G L V
  12 | fquq_bind_dx: ∀a,I,G,L,V,T. fquq G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T
  13 | fquq_flat_dx: ∀I,G, L,V,T. fquq G L (ⓕ{I}V.T) G L T
  14 | fquq_drop   : ∀G,L,K,T,U,k.
  15                 ⬇[k] L ≡ K → ⬆[0, k] T ≡ U → fquq G L U G K T
  16 .