proposition: Lemma z0' : forall l (r: @m idx (nelist T)), compat_prd_unit r -> eval (prd i (run_list (comp (@appne T) l r))) == eval (prd i ((appne (l) (run_list r)))).
proof: Proof. intros. unfold comp. unfold run_list. case_eq r; intros; auto; subst. rewrite eval_prd_app. rewrite eval_prd_nil. apply compat_prd_Unit in H. rewrite law_neutral_right. reflexivity. reflexivity. Qed.
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)