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.ma".
18 (* MULTIPLE FILLING PUSH ****************************************************)
20 (* Properties with multiple filling lift ************************************)
22 lemma mf_vpush_vlift_swap_O (v) (T) (l): ⇡[0←↑[↑l,1]T]⇡[l]v ⊜⇡[↑l]⇡[0←T]v.
24 elim (eq_or_gt i) #Hi destruct
25 [ >mf_vpush_eq >mf_vlift_rw >mf_vpush_eq //
26 | >(mf_vpush_gt … Hi) >mf_vlift_rw >mf_vlift_rw >(mf_vpush_gt … Hi)
31 lemma mf_vpush_vlift_swap_O_lref_O (v) (l): ⇡[0←#0]⇡[l]v ⊜⇡[↑l]⇡[0←#0]v.
32 #v #l @(mf_vpush_vlift_swap_O … (#0))