gistfile1.txt

1: looking for (Equiv (hoD Σ n)) without backtracking
1.1: (*external*) (eapply (ofe_equiv _)) on (Equiv (hoD Σ n)), 0 subgoal(s)
1: looking for (Equiv (hoLtyO Σ n)) without backtracking
1.1: (*external*) (eapply (ofe_equiv _)) on
(Equiv (hoLtyO Σ n)), 0 subgoal(s)
1: looking for (Proper (equiv ==> equiv) packHoLtyO) without backtracking
1: looking for (Params (@packHoLtyO) ?H0) with backtracking
1.1: exact Params_instance_1 on (Params (@packHoLtyO) ?H0), 0 subgoal(s)
1.1: (*external*) proper_reflexive on
(Proper (equiv ==> equiv) packHoLtyO), 1 subgoal(s)
1.1-1 : (Reflexive (equiv ==> equiv)%signature)
1.1-1: looking for (Reflexive (equiv ==> equiv)%signature) without backtracking
1.1-1.1: simple apply @Equivalence_Reflexive on
(Reflexive (equiv ==> equiv)%signature), 1 subgoal(s)
1.1-1.1-1 : (Equivalence (equiv ==> equiv)%signature)
1.1-1.1-1: looking for (Equivalence (equiv ==> equiv)%signature) without backtracking
1.1-1.1-1: no match for (Equivalence (equiv ==> equiv)%signature), 11 possibilities
1.1-1.2: simple apply @PreOrder_Reflexive on
(Reflexive (equiv ==> equiv)%signature), 1 subgoal(s)
1.1-1.2-1 : (PreOrder (equiv ==> equiv)%signature)
1.1-1.2-1: looking for (PreOrder (equiv ==> equiv)%signature) without backtracking
1.1-1.2-1.1: simple apply @partial_order_pre on
(PreOrder (equiv ==> equiv)%signature), 1 subgoal(s)
1.1-1.2-1.1-1 : (PartialOrder (equiv ==> equiv)%signature)
1.1-1.2-1.1-1: looking for (PartialOrder (equiv ==> equiv)%signature) without backtracking
1.1-1.2-1.1-1.1: simple apply @total_order_partial on
(PartialOrder (equiv ==> equiv)%signature), 1 subgoal(s)
1.1-1.2-1.1-1.1-1 : (TotalOrder (equiv ==> equiv)%signature)
1.1-1.2-1.1-1.1-1: looking for (TotalOrder (equiv ==> equiv)%signature) without backtracking
1.1-1.2-1.1-1.1-1: no match for (TotalOrder (equiv ==> equiv)%signature), 0 possibilities
1.1-1.2-1.2: simple apply @Equivalence_PreOrder on
(PreOrder (equiv ==> equiv)%signature), 1 subgoal(s)
1.1-1.2-1.2-1 : (Equivalence (equiv ==> equiv)%signature)
1.1-1.2-1.2-1: looking for (Equivalence (equiv ==> equiv)%signature) without backtracking
1.1-1.2-1.2-1: no match for (Equivalence (equiv ==> equiv)%signature), 11 possibilities
1.2: simple apply @contractive_proper on
(Proper (equiv ==> equiv) packHoLtyO), 1 subgoal(s)
1.2-1 : (Contractive packHoLtyO)
1.2-1: looking for (Contractive packHoLtyO) without backtracking
1.2-1.1: simple apply @packHoLtyO_contractive on
(Contractive packHoLtyO), 0 subgoal(s)