File "./output/relaxed_ambiguous_paths.v", line 13, characters 0-29:
Warning:
New coercion path [g1; f2] : A >-> B' is ambiguous with existing 
[f1; g2] : A >-> B'. [ambiguous-paths,coercions,default]
File "./output/relaxed_ambiguous_paths.v", line 14, characters 0-29:
Warning:
New coercion path [h1; f3] : B >-> C' is ambiguous with existing 
[f2; h2] : B >-> C'. [ambiguous-paths,coercions,default]
[f1] : A >-> A'
[g1] : A >-> B
[f1; g2] : A >-> B'
[g1; h1] : A >-> C
[f1; g2; h2] : A >-> C'
[g2] : A' >-> B'
[g2; h2] : A' >-> C'
[f2] : B >-> B'
[h1] : B >-> C
[f2; h2] : B >-> C'
[h2] : B' >-> C'
[f3] : C >-> C'
[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
File "./output/relaxed_ambiguous_paths.v", line 33, characters 0-28:
Warning:
New coercion path [ab; bc] : A >-> C is ambiguous with existing 
[ac] : A >-> C. [ambiguous-paths,coercions,default]
[ab] : A >-> B
[ac] : A >-> C
[ac; cd] : A >-> D
[bc] : B >-> C
[bc; cd] : B >-> D
[cd] : C >-> D
[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
File "./output/relaxed_ambiguous_paths.v", line 50, characters 0-28:
Warning:
New coercion path [ab; bc] : A >-> C is ambiguous with existing 
[ac] : A >-> C. [ambiguous-paths,coercions,default]
File "./output/relaxed_ambiguous_paths.v", line 51, characters 0-28:
Warning:
New coercion path [ba; ab] : B >-> B is not definitionally an identity function.
New coercion path [ab; ba] : A >-> A is not definitionally an identity function.
[ambiguous-paths,coercions,default]
[ab] : A >-> B
[ac] : A >-> C
[ba] : B >-> A
[bc] : B >-> C
[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
[B_A] : B >-> A
[C_A] : C >-> A
[D_A] : D >-> A
[D_B] : D >-> B
[D_C] : D >-> C
[A'_A] : A' >-> A
[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
[B_A'; A'_A] : B >-> A
[B_A'] : B >-> A'
[C_A'; A'_A] : C >-> A
[C_A'] : C >-> A'
[D_A] : D >-> A
[D_B; B_A'] : D >-> A'
[D_B] : D >-> B
[D_C] : D >-> C
File "./output/relaxed_ambiguous_paths.v", line 147, characters 0-86:
Warning:
New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing 
[D_B; B_A'] : D >-> A'. [ambiguous-paths,coercions,default]
[reverse_coercion] : ReverseCoercionSource >-> ReverseCoercionTarget
[A'_A] : A' >-> A
[B_A'; A'_A] : B >-> A
[B_A'] : B >-> A'
[C_A'; A'_A] : C >-> A
[C_A'] : C >-> A'
[D_A] : D >-> A
[D_B; B_A'] : D >-> A'
[D_B] : D >-> B
[D_C] : D >-> C
File "./output/relaxed_ambiguous_paths.v", line 156, characters 0-47:
Warning:
New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT is not definitionally an identity function.
[ambiguous-paths,coercions,default]
File "./output/relaxed_ambiguous_paths.v", line 157, characters 0-64:
Warning:
New coercion path [unwrap_list; wrap_list] : LIST >-> LIST is not definitionally an identity function.
[ambiguous-paths,coercions,default]
File "./output/relaxed_ambiguous_paths.v", line 158, characters 0-51:
Warning:
New coercion path [unwrap_Type; wrap_Type] : TYPE >-> TYPE is not definitionally an identity function.
[ambiguous-paths,coercions,default]