matita/matita/contribs/lambdadelta/delayed_updating/etc/prototerm_constructors.etc

   1 (* COMMENT
   2 lemma prototerm_in_root_inv_lcons_oref:
   3       ∀p,l,n. l◗p ϵ ▵#n →
   4       ∧∧ 𝗱n = l & 𝐞 = p.
   5 #p #l #n * #q
   6 <list_append_lcons_sn #H0 destruct -H0
   7 elim (eq_inv_list_empty_append … e0) -e0 #H0 #_
   8 /2 width=1 by conj/
   9 qed-.
  10
  11 lemma prototerm_in_root_inv_lcons_iref:
  12       ∀t,p,l,n. l◗p ϵ ▵𝛕n.t →
  13       ∧∧ 𝗱n = l & p ϵ ▵ɱ.t.
  14 #t #p #l #n * #q * #r #Hr
  15 <list_append_lcons_sn #H0 destruct -H0
  16 /4 width=4 by ex2_intro, ex_intro, conj/
  17 qed-.
  18
  19 lemma prototerm_in_root_inv_lcons_mark:
  20       ∀t,p,l. l◗p ϵ ▵ɱ.t →
  21       ∧∧ 𝗺 = l & p ϵ ▵t.
  22 #t #p #l * #q * #r #Hr
  23 <list_append_lcons_sn #H0 destruct
  24 /3 width=2 by ex_intro, conj/
  25 qed-.
  26
  27 lemma prototerm_in_root_inv_lcons_abst:
  28       ∀t,p,l. l◗p ϵ ▵𝛌.t →
  29       ∧∧ 𝗟 = l & p ϵ ▵t.
  30 #t #p #l * #q * #r #Hr
  31 <list_append_lcons_sn #H0 destruct
  32 /3 width=2 by ex_intro, conj/
  33 qed-.
  34
  35 lemma prototerm_in_root_inv_lcons_appl:
  36       ∀u,t,p,l. l◗p ϵ ▵@u.t →
  37       ∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
  38        | ∧∧ 𝗔 = l & p ϵ ▵t.
  39 #u #t #p #l * #q * * #r #Hr
  40 <list_append_lcons_sn #H0 destruct
  41 /4 width=2 by ex_intro, or_introl, or_intror, conj/
  42 qed-.
  43 *)