matita/matita/contribs/lambdadelta/static_2/etc/teqx/req_length.etc

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "static_2/static/rex_length.ma".
  16 include "static_2/static/rex_fsle.ma".
  17 include "static_2/static/req.ma".
  18
  19 (* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
  20
  21 (* Advanved properties with free variables inclusion ************************)
  22
  23 lemma req_fsge_comp:
  24       rex_fsge_compatible ceq.
  25 #L1 #L2 #T #H elim H #f1 #Hf1 #HL12
  26 lapply (frees_req_conf … Hf1 … H) -H
  27 lapply (sex_fwd_length … HL12)
  28 /3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *)
  29 qed-.
  30
  31 (* Advanced properties ******************************************************)
  32
  33 (* Basic_2A1: uses: lleq_sym *)
  34 lemma req_sym (T):
  35       symmetric … (req T).
  36 /3 width=1 by req_fsge_comp, rex_sym/ qed-.