fact: Definition RLiteralNonConstructor_beq {t1 t2} (e1 : RLiteralNonConstructor t1) (e2 : RLiteralNonConstructor t2) : bool := match e1, e2 with | Rfst A B, Rfst A' B' => SimpleTypeCode_beq A A' && SimpleTypeCode_beq B B' | Rfst _ _, _ => false | Rsnd A B, Rsnd A' B' => SimpleTypeCode_beq A A' && SimpleTypeCode_beq B B' | Rsnd _ _, _ => false | Rnth' A, Rnth' A' => SimpleTypeCode_beq A A' | Rnth' _, _ => false | Rnth A, Rnth A' => SimpleTypeCode_beq A A' | Rnth _, _ => false | Rbeq_nat, Rbeq_nat => true | Rbeq_nat, _ => false | Rmap A B, Rmap A' B' => SimpleTypeCode_beq A A' && SimpleTypeCode_beq B B' | Rmap _ _, _ => false | Rfold_left A B, Rfold_left A' B' => SimpleTypeCode_beq A A' && SimpleTypeCode_beq B B' | Rfold_left _ _, _ => false | Rorb, Rorb => true | Rorb, _ => false | Randb, Randb => true | Randb, _ => false | Randbr, Randbr => true | Randbr, _ => false | Rorbr, Rorbr => true | Rorbr, _ => false | Rminusr, Rminusr => true | Rminusr, _ => false | Rpred, Rpred => true | Rpred, _ => false | Rlength A, Rlength A' => SimpleTypeCode_beq A A' | Rlength _, _ => false | Rbool_rect_nodep A, Rbool_rect_nodep A' => SimpleTypeCode_beq A A' | Rbool_rect_nodep _, _ => false | Rlist_rect_nodep A P, Rlist_rect_nodep A' P' => SimpleTypeCode_beq A A' && TypeCode_beq P P' | Rlist_rect_nodep _ _, _ => false | Rlist_caset_nodep A P, Rlist_caset_nodep A' P' => SimpleTypeCode_beq A A' && SimpleTypeCode_beq P P' | Rlist_caset_nodep _ _, _ => false | Rleb, Rleb => true | Rleb, _ => false | Rcombine A B, Rcombine A' B' => SimpleTypeCode_beq A A' && SimpleTypeCode_beq B B' | Rcombine _ _, _ => false | Rrev A, Rrev A' => SimpleTypeCode_beq A A' | Rrev _, _ => false | Rup_to, Rup_to => true | Rup_to, _ => false | Rplus, Rplus => true | Rplus, _ => false | Rmax, Rmax => true | Rmax, _ => false | Rritem_rect_nodep A, Rritem_rect_nodep A' => SimpleTypeCode_beq A A' | Rritem_rect_nodep _, _ => false | Rfirst_index_default A, Rfirst_index_default A' => SimpleTypeCode_beq A A' | Rfirst_index_default _, _ => false | Rinterp_RCharExpr_ascii, Rinterp_RCharExpr_ascii => true | Rinterp_RCharExpr_ascii, _ => false | Rstring_beq, Rstring_beq => true | Rstring_beq, _ => false end%bool.
imports: Coq.Strings.Ascii Fiat.Parsers.Reflective.Syntax Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Common.Equality Fiat.Common.BoolFacts