proposition: Lemma extend_equiv : forall val val' n P, (forall m, equiv_comp_pair (val m) (val' m)) -> forall k, equiv_comp_pair (extend val n P k) (extend val' n P k).
proof: Proof. intros. unfold extend. destruct (k =? n); simpl; auto. Qed.
imports: List Arith Bool