]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/syntax/teqw_teqw.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / teqw_teqw.ma
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/syntax/teqw.ma".
16
17 (* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************)
18
19 (* Main properties **********************************************************)
20
21 theorem teqw_trans: Transitive … teqw.
22 #T1 #T #H elim H -T1 -T
23 [ #s1 #s #X #H
24   elim (teqw_inv_sort_sn … H) -s #s2 destruct
25   /2 width=1 by teqw_sort/
26 | #i1 #i #H //
27 | #l1 #l #H //
28 | #p #V1 #V #T1 #T #_ #IHT #X #H
29   elim (teqw_inv_abbr_sn … H) -H #V2 #T2 #HT #H destruct
30   /4 width=1 by teqw_abbr/
31 | #p #V1 #V #T1 #T #X #H
32   elim (teqw_inv_abst_sn … H) -H #V2 #T2 #H destruct
33   /2 width=1 by teqw_abst/
34 | #V1 #V #T1 #T #_ #IHT #X #H
35   elim (teqw_inv_appl_sn … H) -H #V2 #T2 #HT #H destruct
36   /3 width=1 by teqw_appl/
37 | #V1 #V #T1 #T #_ #_ #IHV #IHT #X #H
38   elim (teqw_inv_cast_sn … H) -H #V2 #T2 #HV #HT #H destruct
39   /3 width=1 by teqw_cast/
40 ]
41 qed-.
42
43 theorem teqw_canc_sn: left_cancellable … teqw.
44 /3 width=3 by teqw_trans, teqw_sym/ qed-.
45
46 theorem teqw_canc_dx: right_cancellable … teqw.
47 /3 width=3 by teqw_trans, teqw_sym/ qed-.
48
49 theorem teqw_repl:
50         ∀T1,T2. T1 ≃ T2 → ∀U1. T1 ≃ U1 → ∀U2. T2 ≃ U2 → U1 ≃ U2.
51 /3 width=3 by teqw_canc_sn, teqw_trans/ qed-.