fact: Hypothesis is_unit_prd_Unit : forall j, is_unit j = true -> @Unit X R (Bin.value (e_bin i)) (eval (unit j)).
imports: Coq(Arith NArith List) Coq(FMapPositive Relations RelationClasses) AAC_tactics(Utils Constants)