proposition: Lemma precondition_shift : forall m i a a', (forall g, i_a m g a -> i_a m g a') -> forall g, i_a m g (pc i a)-> i_a m g (pc i a').
proof: Proof. intros m'; induction i; simpl; auto. intros a a' Haa' g; repeat rewrite a_subst_fpw. apply Haa'. intros a a' Haa' g; apply IHi1; apply IHi2; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom