proposition: Lemma vcg_shift : forall m i p q, (forall g, i_lc m g (vcg i p)) -> (forall g, i_c m g (c_imp p q)) -> forall g, (i_c m g (c_imp (pc i p) (pc i q)) /\ i_lc m g (vcg i q)).
proof: Proof. intros m' i; induction i. simpl; intros p q Hv Hpq g; split; auto. assert (Hi' := IHi p q). assert (Hv2 : forall g, i_lc m' g (vcg i p)) by (intros g'; elim (Hv g'); auto). destruct (Hi' Hv2 Hpq g) as [Hi1 Hi2]; simpl in Hi1; clear Hi'. split; elim (Hv g); auto. simpl; intros p q Hv Hpq g; split; auto. simpl; intros p q Hv Hpq g; split; auto. repeat rewrite a_subst_fpw; auto. simpl; intros p q Hv Hpq g; auto. assert (IHi2' := IHi2 p q). assert (Hv1 : forall g, i_lc m' g (vcg i2 p)). intros g'; apply i_lc_app_l with (1:= Hv g'). assert (Hi2_1 : forall g, i_c m' g (c_imp (pc i2 p)(pc i2 q))). intros g'; elim (IHi2' Hv1 Hpq g'); auto. assert (Hv2 : forall g, i_lc m' g (vcg i1 (pc i2 p))). intros g'; apply i_lc_app_r with (1:= Hv g'). destruct (IHi1 (pc i2 p)(pc i2 q) Hv2 Hi2_1 g) as [Hi1_1 Hi1_2]. split;[exact Hi1_1 | apply app_i_lc; auto]. elim (IHi2' Hv1 Hpq g); auto. simpl; intros p q Hv Hpq; intros g; split. auto. destruct (Hv g) as [Hv1 [Hv2 Hv3]]. split. intros; apply Hpq; auto. auto. Qed.
imports: syntax little denot Bool List String ZArith axiom