1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "apps_2/functional/mf_vlift_exteq.ma".
16 include "apps_2/functional/mf_vpush_exteq.ma".
17 include "apps_2/functional/mf.ma".
19 (* MULTIPLE FILLING FOR TERMS ***********************************************)
21 (* Properties with extensional equivalence **********************************)
23 lemma mf_comp (T): compatible_3 … (λgv,lv.■[gv,lv]T) (exteq …) (exteq …) (eq …).
26 | #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
28 | #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
30 | #p #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
31 whd in ⊢ (??%%); /4 width=1 by mf_vlift_comp, mf_vpush_comp, eq_f3/
32 | #I #V #T #IHV #IHT #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
33 whd in ⊢ (??%%); /3 width=1 by eq_f3/
37 (* Advanced properties ******************************************************)
39 lemma mf_id (T): ■[mf_gi,mf_li]T = T.
41 [ #p #I #V #T #IHV #IHT
42 <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT
43 whd in ⊢ (??%?); /3 width=1 by mf_comp, eq_f3/
45 <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT //