fact: Fixpoint binary_word_or (n:nat)(w1:binary_word n) {struct w1}: binary_word n -> binary_word n := match w1 in binary_word p return binary_word p -> binary_word p with bw0 => (fun w2:binary_word 0 => match w2 in binary_word p' return p'=0->binary_word p' with bw0 => (fun h => bw0) | bwS q b w2' => (fun h => False_rec (binary_word (S q)) (discriminate_S_O h)) end (refl_equal 0)) | bwS q b1 w1' => (fun w2:binary_word (S q) => match w2 in binary_word p' return S q=p'->binary_word p' with bw0 => (fun h => False_rec (binary_word 0) (discriminate_S_O h)) | bwS q' b2 w2' => (fun h => bwS q' (orb b1 b2) (binary_word_or q' (eq_rec (S q) (fun v:nat => binary_word (pred v)) w1' (S q') (h:S q=S q')) w2')) end (refl_equal (S q))) end.
imports: Bool