proposition: Lemma R1_lem3 : forall t : nat, t < size -> abit (R1 t) 0 = abit V1 t.
proof: Proof. intros. unfold abit in |- *. unfold elemlist in |- *. apply (trunc_plus_petit bool) with (size - t). unfold lt in H. inversion H. rewrite <- minus_Sn_m. auto with arith. auto with arith. rewrite <- minus_Sn_m. auto with arith. apply le_Sn_le; auto with arith. rewrite (strip_O bool). apply R1_lem. apply lt_le_weak. exact H. Qed.
imports: Definitions