fact: Fixpoint sigma_get default m i := match m with | N l o r => match i with | xH => match o with None => default | Some a => a end | xO i => sigma_get default l i | xI i => sigma_get default r i end | _ => default end.
imports: BinNums comparisons