proposition: Theorem LH_Gn_1_equiv : forall (n : nat) c, n < numA -> evalDist (LH_Gn (S n)) c == evalDist (LH_G_1 n) c.
proof: Proof. intuition. unfold LH_Gn, LH_G_1. comp_skip. comp_simp. rewrite (firstn_S _ defA). assert (evalDist (lsb1 <-$ (foreach (x in firstn n l ++ nth n l defA :: nil) A2' s x); lsb2 <-$ (foreach (x in skipn (S n) l)A2 s x); A3 s (lsb1 ++ lsb2) ) c == evalDist (lsb1 <-$ (r1 <-$ compMap _ (A2' s) (firstn n l); r2 <-$ compMap _ (A2' s) (nth n l defA :: nil); ret (r1 ++ r2)); lsb2 <-$ (foreach (x in skipn (S n) l)A2 s x); A3 s (lsb1 ++ lsb2) ) c ). comp_skip. eapply compMap_app. match goal with [H1:_|- _ ] => rewrite H1; clear H1 end. inline_first. comp_skip. inline_first. comp_skip. inline_first. comp_skip. reflexivity. rewrite <- app_assoc. rewrite <- app_comm_cons. simpl. intuition. erewrite numA_correct; intuition; eauto. Qed.
imports: FCF CompFold